Metamath Proof Explorer

Theorem elaltxp

Description: Membership in alternate Cartesian products. (Contributed by Scott Fenton, 23-Mar-2012)

Ref Expression
Assertion elaltxp ⊢ X ∈ A ×× B ↔ ∃ x ∈ A ∃ y ∈ B X = x y

Proof

Step Hyp Ref Expression
1 elex ⊢ X ∈ A ×× B → X ∈ V
2 altopex ⊢ x y ∈ V
3 eleq1 ⊢ X = x y → X ∈ V ↔ x y ∈ V
4 2 3 mpbiri ⊢ X = x y → X ∈ V
5 4 a1i ⊢ x ∈ A ∧ y ∈ B → X = x y → X ∈ V
6 5 rexlimivv ⊢ ∃ x ∈ A ∃ y ∈ B X = x y → X ∈ V
7 eqeq1 ⊢ z = X → z = x y ↔ X = x y
8 7 2rexbidv ⊢ z = X → ∃ x ∈ A ∃ y ∈ B z = x y ↔ ∃ x ∈ A ∃ y ∈ B X = x y
9 df-altxp ⊢ A ×× B = z | ∃ x ∈ A ∃ y ∈ B z = x y
10 8 9 elab2g ⊢ X ∈ V → X ∈ A ×× B ↔ ∃ x ∈ A ∃ y ∈ B X = x y
11 1 6 10 pm5.21nii ⊢ X ∈ A ×× B ↔ ∃ x ∈ A ∃ y ∈ B X = x y