Theorem opelxp

Description: Ordered pair membership in a Cartesian product. (Contributed by NM, 15-Nov-1994) (Proof shortened by Andrew Salmon, 12-Aug-2011) (Revised by Mario Carneiro, 26-Apr-2015)

	Ref	Expression
Assertion	opelxp	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝐶 × 𝐷 ) ↔ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		elxp2	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝐶 × 𝐷 ) ↔ ∃ 𝑥 ∈ 𝐶 ∃ 𝑦 ∈ 𝐷 ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
2		vex	⊢ 𝑥 ∈ V
3		vex	⊢ 𝑦 ∈ V
4	2 3	opth2	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ↔ ( 𝐴 = 𝑥 ∧ 𝐵 = 𝑦 ) )
5		eleq1	⊢ ( 𝐴 = 𝑥 → ( 𝐴 ∈ 𝐶 ↔ 𝑥 ∈ 𝐶 ) )
6		eleq1	⊢ ( 𝐵 = 𝑦 → ( 𝐵 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷 ) )
7	5 6	bi2anan9	⊢ ( ( 𝐴 = 𝑥 ∧ 𝐵 = 𝑦 ) → ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) ↔ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ) )
8	4 7	sylbi	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) ↔ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ) )
9	8	biimprcd	⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) → ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) ) )
10	9	rexlimivv	⊢ ( ∃ 𝑥 ∈ 𝐶 ∃ 𝑦 ∈ 𝐷 ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) )
11		eqid	⊢ ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐴 , 𝐵 ⟩
12		opeq1	⊢ ( 𝑥 = 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐴 , 𝑦 ⟩ )
13	12	eqeq2d	⊢ ( 𝑥 = 𝐴 → ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ↔ ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐴 , 𝑦 ⟩ ) )
14		opeq2	⊢ ( 𝑦 = 𝐵 → ⟨ 𝐴 , 𝑦 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
15	14	eqeq2d	⊢ ( 𝑦 = 𝐵 → ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐴 , 𝑦 ⟩ ↔ ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ) )
16	13 15	rspc2ev	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ) → ∃ 𝑥 ∈ 𝐶 ∃ 𝑦 ∈ 𝐷 ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
17	11 16	mp3an3	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ∃ 𝑥 ∈ 𝐶 ∃ 𝑦 ∈ 𝐷 ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
18	10 17	impbii	⊢ ( ∃ 𝑥 ∈ 𝐶 ∃ 𝑦 ∈ 𝐷 ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ↔ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) )
19	1 18	bitri	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝐶 × 𝐷 ) ↔ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) )