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

Metamath Proof Explorer

Theorem op1steq

Description: Two ways of expressing that an element is the first member of an ordered pair. (Contributed by NM, 22-Sep-2013) (Revised by Mario Carneiro, 23-Feb-2014)

		Ref	Expression
	Assertion	op1steq	⊢ ( 𝐴 ∈ ( 𝑉 × 𝑊 ) → ( ( 1^st ‘ 𝐴 ) = 𝐵 ↔ ∃ 𝑥 𝐴 = ⟨ 𝐵 , 𝑥 ⟩ ) )

Proof

Step	Hyp	Ref	Expression
1		xpss	⊢ ( 𝑉 × 𝑊 ) ⊆ ( V × V )
2	1	sseli	⊢ ( 𝐴 ∈ ( 𝑉 × 𝑊 ) → 𝐴 ∈ ( V × V ) )
3		eqid	⊢ ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ 𝐴 )
4		eqopi	⊢ ( ( 𝐴 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝐴 ) = 𝐵 ∧ ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ 𝐴 ) ) ) → 𝐴 = ⟨ 𝐵 , ( 2^nd ‘ 𝐴 ) ⟩ )
5	3 4	mpanr2	⊢ ( ( 𝐴 ∈ ( V × V ) ∧ ( 1^st ‘ 𝐴 ) = 𝐵 ) → 𝐴 = ⟨ 𝐵 , ( 2^nd ‘ 𝐴 ) ⟩ )
6		fvex	⊢ ( 2^nd ‘ 𝐴 ) ∈ V
7		opeq2	⊢ ( 𝑥 = ( 2^nd ‘ 𝐴 ) → ⟨ 𝐵 , 𝑥 ⟩ = ⟨ 𝐵 , ( 2^nd ‘ 𝐴 ) ⟩ )
8	7	eqeq2d	⊢ ( 𝑥 = ( 2^nd ‘ 𝐴 ) → ( 𝐴 = ⟨ 𝐵 , 𝑥 ⟩ ↔ 𝐴 = ⟨ 𝐵 , ( 2^nd ‘ 𝐴 ) ⟩ ) )
9	6 8	spcev	⊢ ( 𝐴 = ⟨ 𝐵 , ( 2^nd ‘ 𝐴 ) ⟩ → ∃ 𝑥 𝐴 = ⟨ 𝐵 , 𝑥 ⟩ )
10	5 9	syl	⊢ ( ( 𝐴 ∈ ( V × V ) ∧ ( 1^st ‘ 𝐴 ) = 𝐵 ) → ∃ 𝑥 𝐴 = ⟨ 𝐵 , 𝑥 ⟩ )
11	10	ex	⊢ ( 𝐴 ∈ ( V × V ) → ( ( 1^st ‘ 𝐴 ) = 𝐵 → ∃ 𝑥 𝐴 = ⟨ 𝐵 , 𝑥 ⟩ ) )
12		eqop	⊢ ( 𝐴 ∈ ( V × V ) → ( 𝐴 = ⟨ 𝐵 , 𝑥 ⟩ ↔ ( ( 1^st ‘ 𝐴 ) = 𝐵 ∧ ( 2^nd ‘ 𝐴 ) = 𝑥 ) ) )
13		simpl	⊢ ( ( ( 1^st ‘ 𝐴 ) = 𝐵 ∧ ( 2^nd ‘ 𝐴 ) = 𝑥 ) → ( 1^st ‘ 𝐴 ) = 𝐵 )
14	12 13	biimtrdi	⊢ ( 𝐴 ∈ ( V × V ) → ( 𝐴 = ⟨ 𝐵 , 𝑥 ⟩ → ( 1^st ‘ 𝐴 ) = 𝐵 ) )
15	14	exlimdv	⊢ ( 𝐴 ∈ ( V × V ) → ( ∃ 𝑥 𝐴 = ⟨ 𝐵 , 𝑥 ⟩ → ( 1^st ‘ 𝐴 ) = 𝐵 ) )
16	11 15	impbid	⊢ ( 𝐴 ∈ ( V × V ) → ( ( 1^st ‘ 𝐴 ) = 𝐵 ↔ ∃ 𝑥 𝐴 = ⟨ 𝐵 , 𝑥 ⟩ ) )
17	2 16	syl	⊢ ( 𝐴 ∈ ( 𝑉 × 𝑊 ) → ( ( 1^st ‘ 𝐴 ) = 𝐵 ↔ ∃ 𝑥 𝐴 = ⟨ 𝐵 , 𝑥 ⟩ ) )