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

Metamath Proof Explorer

Theorem 1stval2

Description: Alternate value of the function that extracts the first member of an ordered pair. Definition 5.13 (i) of Monk1 p. 52. (Contributed by NM, 18-Aug-2006)

		Ref	Expression
	Assertion	1stval2	⊢ ( 𝐴 ∈ ( V × V ) → ( 1^st ‘ 𝐴 ) = ∩ ∩ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		elvv	⊢ ( 𝐴 ∈ ( V × V ) ↔ ∃ 𝑥 ∃ 𝑦 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ )
2		vex	⊢ 𝑥 ∈ V
3		vex	⊢ 𝑦 ∈ V
4	2 3	op1st	⊢ ( 1^st ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑥
5	2 3	op1stb	⊢ ∩ ∩ ⟨ 𝑥 , 𝑦 ⟩ = 𝑥
6	4 5	eqtr4i	⊢ ( 1^st ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = ∩ ∩ ⟨ 𝑥 , 𝑦 ⟩
7		fveq2	⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 1^st ‘ 𝐴 ) = ( 1^st ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
8		inteq	⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ∩ 𝐴 = ∩ ⟨ 𝑥 , 𝑦 ⟩ )
9	8	inteqd	⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ∩ ∩ 𝐴 = ∩ ∩ ⟨ 𝑥 , 𝑦 ⟩ )
10	6 7 9	3eqtr4a	⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 1^st ‘ 𝐴 ) = ∩ ∩ 𝐴 )
11	10	exlimivv	⊢ ( ∃ 𝑥 ∃ 𝑦 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 1^st ‘ 𝐴 ) = ∩ ∩ 𝐴 )
12	1 11	sylbi	⊢ ( 𝐴 ∈ ( V × V ) → ( 1^st ‘ 𝐴 ) = ∩ ∩ 𝐴 )