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	$$⊢A\in \left(\mathrm{V}\times \mathrm{V}\right)\to 1^{st}\left(A\right)=\bigcap \bigcap A$$

Proof

Step	Hyp	Ref	Expression
1		elvv	$$⊢A\in \left(\mathrm{V}\times \mathrm{V}\right)\leftrightarrow \exists x\exists yA=⟨x,y⟩$$
2		vex	$$⊢x\in \mathrm{V}$$
3		vex	$$⊢y\in \mathrm{V}$$
4	2 3	op1st	$$⊢1^{st}\left(⟨x,y⟩\right)=x$$
5	2 3	op1stb	$$⊢\bigcap \bigcap ⟨x,y⟩=x$$
6	4 5	eqtr4i	$$⊢1^{st}\left(⟨x,y⟩\right)=\bigcap \bigcap ⟨x,y⟩$$
7		fveq2	$$⊢A=⟨x,y⟩\to 1^{st}\left(A\right)=1^{st}\left(⟨x,y⟩\right)$$
8		inteq	$$⊢A=⟨x,y⟩\to \bigcap A=\bigcap ⟨x,y⟩$$
9	8	inteqd	$$⊢A=⟨x,y⟩\to \bigcap \bigcap A=\bigcap \bigcap ⟨x,y⟩$$
10	6 7 9	3eqtr4a	$$⊢A=⟨x,y⟩\to 1^{st}\left(A\right)=\bigcap \bigcap A$$
11	10	exlimivv	$$⊢\exists x\exists yA=⟨x,y⟩\to 1^{st}\left(A\right)=\bigcap \bigcap A$$
12	1 11	sylbi	$$⊢A\in \left(\mathrm{V}\times \mathrm{V}\right)\to 1^{st}\left(A\right)=\bigcap \bigcap A$$