This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elxp6

Description: Membership in a Cartesian product. This version requires no quantifiers or dummy variables. See also elxp4 . (Contributed by NM, 9-Oct-2004)

		Ref	Expression
	Assertion	elxp6	⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) ↔ ( 𝐴 = ⟨ ( 1^st ‘ 𝐴 ) , ( 2^nd ‘ 𝐴 ) ⟩ ∧ ( ( 1^st ‘ 𝐴 ) ∈ 𝐵 ∧ ( 2^nd ‘ 𝐴 ) ∈ 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elxp4	⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) ↔ ( 𝐴 = ⟨ ∪ dom { 𝐴 } , ∪ ran { 𝐴 } ⟩ ∧ ( ∪ dom { 𝐴 } ∈ 𝐵 ∧ ∪ ran { 𝐴 } ∈ 𝐶 ) ) )
2		1stval	⊢ ( 1^st ‘ 𝐴 ) = ∪ dom { 𝐴 }
3		2ndval	⊢ ( 2^nd ‘ 𝐴 ) = ∪ ran { 𝐴 }
4	2 3	opeq12i	⊢ ⟨ ( 1^st ‘ 𝐴 ) , ( 2^nd ‘ 𝐴 ) ⟩ = ⟨ ∪ dom { 𝐴 } , ∪ ran { 𝐴 } ⟩
5	4	eqeq2i	⊢ ( 𝐴 = ⟨ ( 1^st ‘ 𝐴 ) , ( 2^nd ‘ 𝐴 ) ⟩ ↔ 𝐴 = ⟨ ∪ dom { 𝐴 } , ∪ ran { 𝐴 } ⟩ )
6	2	eleq1i	⊢ ( ( 1^st ‘ 𝐴 ) ∈ 𝐵 ↔ ∪ dom { 𝐴 } ∈ 𝐵 )
7	3	eleq1i	⊢ ( ( 2^nd ‘ 𝐴 ) ∈ 𝐶 ↔ ∪ ran { 𝐴 } ∈ 𝐶 )
8	6 7	anbi12i	⊢ ( ( ( 1^st ‘ 𝐴 ) ∈ 𝐵 ∧ ( 2^nd ‘ 𝐴 ) ∈ 𝐶 ) ↔ ( ∪ dom { 𝐴 } ∈ 𝐵 ∧ ∪ ran { 𝐴 } ∈ 𝐶 ) )
9	5 8	anbi12i	⊢ ( ( 𝐴 = ⟨ ( 1^st ‘ 𝐴 ) , ( 2^nd ‘ 𝐴 ) ⟩ ∧ ( ( 1^st ‘ 𝐴 ) ∈ 𝐵 ∧ ( 2^nd ‘ 𝐴 ) ∈ 𝐶 ) ) ↔ ( 𝐴 = ⟨ ∪ dom { 𝐴 } , ∪ ran { 𝐴 } ⟩ ∧ ( ∪ dom { 𝐴 } ∈ 𝐵 ∧ ∪ ran { 𝐴 } ∈ 𝐶 ) ) )
10	1 9	bitr4i	⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) ↔ ( 𝐴 = ⟨ ( 1^st ‘ 𝐴 ) , ( 2^nd ‘ 𝐴 ) ⟩ ∧ ( ( 1^st ‘ 𝐴 ) ∈ 𝐵 ∧ ( 2^nd ‘ 𝐴 ) ∈ 𝐶 ) ) )