Proof 01. 1 ⊢ set A, hypo. 02. 2 ⊢ set B, hypo. 03. 1, 2 ⊢ set (A ∪ B), set_union 1 2. 04. 1, 2 ⊢ set (power (A ∪ B)), power 3. 05. 1, 2 ⊢ set (power (power (A ∪ B))), power 4. 06. 1, 2 ⊢ set (A × B), subset prod_incl_in_power 5. set_prod. ⊢ set A → set B → set (A × B), subj_intro_ii 6.
Dependencies
The given proof depends on eight axioms:
comp, eq_refl, eq_subst, ext, pairing, power, subset, union.