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

Metamath Proof Explorer

Theorem elxp7

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

		Ref	Expression
	Assertion	elxp7	⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) ↔ ( 𝐴 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝐴 ) ∈ 𝐵 ∧ ( 2^nd ‘ 𝐴 ) ∈ 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elxp6	⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) ↔ ( 𝐴 = ⟨ ( 1^st ‘ 𝐴 ) , ( 2^nd ‘ 𝐴 ) ⟩ ∧ ( ( 1^st ‘ 𝐴 ) ∈ 𝐵 ∧ ( 2^nd ‘ 𝐴 ) ∈ 𝐶 ) ) )
2		fvex	⊢ ( 1^st ‘ 𝐴 ) ∈ V
3		fvex	⊢ ( 2^nd ‘ 𝐴 ) ∈ V
4	2 3	pm3.2i	⊢ ( ( 1^st ‘ 𝐴 ) ∈ V ∧ ( 2^nd ‘ 𝐴 ) ∈ V )
5		elxp6	⊢ ( 𝐴 ∈ ( V × V ) ↔ ( 𝐴 = ⟨ ( 1^st ‘ 𝐴 ) , ( 2^nd ‘ 𝐴 ) ⟩ ∧ ( ( 1^st ‘ 𝐴 ) ∈ V ∧ ( 2^nd ‘ 𝐴 ) ∈ V ) ) )
6	4 5	mpbiran2	⊢ ( 𝐴 ∈ ( V × V ) ↔ 𝐴 = ⟨ ( 1^st ‘ 𝐴 ) , ( 2^nd ‘ 𝐴 ) ⟩ )
7	6	anbi1i	⊢ ( ( 𝐴 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝐴 ) ∈ 𝐵 ∧ ( 2^nd ‘ 𝐴 ) ∈ 𝐶 ) ) ↔ ( 𝐴 = ⟨ ( 1^st ‘ 𝐴 ) , ( 2^nd ‘ 𝐴 ) ⟩ ∧ ( ( 1^st ‘ 𝐴 ) ∈ 𝐵 ∧ ( 2^nd ‘ 𝐴 ) ∈ 𝐶 ) ) )
8	1 7	bitr4i	⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) ↔ ( 𝐴 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝐴 ) ∈ 𝐵 ∧ ( 2^nd ‘ 𝐴 ) ∈ 𝐶 ) ) )