Theorem altopelaltxp

Description: Alternate ordered pair membership in a Cartesian product. Note that, unlike opelxp , there is no sethood requirement here. (Contributed by Scott Fenton, 22-Mar-2012)

	Ref	Expression
Assertion	altopelaltxp	⊢ ( ⟪ 𝑋 , 𝑌 ⟫ ∈ ( 𝐴 ×× 𝐵 ) ↔ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		elaltxp	⊢ ( ⟪ 𝑋 , 𝑌 ⟫ ∈ ( 𝐴 ×× 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ⟪ 𝑋 , 𝑌 ⟫ = ⟪ 𝑥 , 𝑦 ⟫ )
2		reeanv	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝑥 = 𝑋 ∧ ∃ 𝑦 ∈ 𝐵 𝑦 = 𝑌 ) )
3		eqcom	⊢ ( ⟪ 𝑋 , 𝑌 ⟫ = ⟪ 𝑥 , 𝑦 ⟫ ↔ ⟪ 𝑥 , 𝑦 ⟫ = ⟪ 𝑋 , 𝑌 ⟫ )
4		vex	⊢ 𝑥 ∈ V
5		vex	⊢ 𝑦 ∈ V
6	4 5	altopth	⊢ ( ⟪ 𝑥 , 𝑦 ⟫ = ⟪ 𝑋 , 𝑌 ⟫ ↔ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) )
7	3 6	bitri	⊢ ( ⟪ 𝑋 , 𝑌 ⟫ = ⟪ 𝑥 , 𝑦 ⟫ ↔ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) )
8	7	2rexbii	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ⟪ 𝑋 , 𝑌 ⟫ = ⟪ 𝑥 , 𝑦 ⟫ ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) )
9		risset	⊢ ( 𝑋 ∈ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 𝑥 = 𝑋 )
10		risset	⊢ ( 𝑌 ∈ 𝐵 ↔ ∃ 𝑦 ∈ 𝐵 𝑦 = 𝑌 )
11	9 10	anbi12i	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝑥 = 𝑋 ∧ ∃ 𝑦 ∈ 𝐵 𝑦 = 𝑌 ) )
12	2 8 11	3bitr4i	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ⟪ 𝑋 , 𝑌 ⟫ = ⟪ 𝑥 , 𝑦 ⟫ ↔ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) )
13	1 12	bitri	⊢ ( ⟪ 𝑋 , 𝑌 ⟫ ∈ ( 𝐴 ×× 𝐵 ) ↔ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) )