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

Proof

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