Theorem elxp2

Description: Membership in a Cartesian product. (Contributed by NM, 23-Feb-2004) (Proof shortened by JJ, 13-Aug-2021)

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

Proof

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