Theorem elxp3

Description: Membership in a Cartesian product. (Contributed by NM, 5-Mar-1995)

	Ref	Expression
Assertion	elxp3	⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) ↔ ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ = 𝐴 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elxp	⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) )
2		eqcom	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = 𝐴 ↔ 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ )
3		opelxp	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐶 ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) )
4	2 3	anbi12i	⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ = 𝐴 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐶 ) ) ↔ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) )
5	4	2exbii	⊢ ( ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ = 𝐴 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐶 ) ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) )
6	1 5	bitr4i	⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) ↔ ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ = 𝐴 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐶 ) ) )