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	$⊢ A \in (V \times W) \to (1^{st} (A) = B \leftrightarrow \exists x A = ⟨B, x⟩)$

Proof

Step	Hyp	Ref	Expression
1		xpss	$⊢ V \times W \subseteq V \times V$
2	1	sseli	$⊢ A \in (V \times W) \to A \in (V \times V)$
3		eqid	$⊢ 2^{nd} (A) = 2^{nd} (A)$
4		eqopi	$⊢ (A \in (V \times V) \land (1^{st} (A) = B \land 2^{nd} (A) = 2^{nd} (A))) \to A = ⟨B, 2^{nd} (A)⟩$
5	3 4	mpanr2	$⊢ (A \in (V \times V) \land 1^{st} (A) = B) \to A = ⟨B, 2^{nd} (A)⟩$
6		fvex	$⊢ 2^{nd} (A) \in V$
7		opeq2	$⊢ x = 2^{nd} (A) \to ⟨B, x⟩ = ⟨B, 2^{nd} (A)⟩$
8	7	eqeq2d	$⊢ x = 2^{nd} (A) \to (A = ⟨B, x⟩ \leftrightarrow A = ⟨B, 2^{nd} (A)⟩)$
9	6 8	spcev	$⊢ A = ⟨B, 2^{nd} (A)⟩ \to \exists x A = ⟨B, x⟩$
10	5 9	syl	$⊢ (A \in (V \times V) \land 1^{st} (A) = B) \to \exists x A = ⟨B, x⟩$
11	10	ex	$⊢ A \in (V \times V) \to (1^{st} (A) = B \to \exists x A = ⟨B, x⟩)$
12		eqop	$⊢ A \in (V \times V) \to (A = ⟨B, x⟩ \leftrightarrow (1^{st} (A) = B \land 2^{nd} (A) = x))$
13		simpl	$⊢ (1^{st} (A) = B \land 2^{nd} (A) = x) \to 1^{st} (A) = B$
14	12 13	syl6bi	$⊢ A \in (V \times V) \to (A = ⟨B, x⟩ \to 1^{st} (A) = B)$
15	14	exlimdv	$⊢ A \in (V \times V) \to (\exists x A = ⟨B, x⟩ \to 1^{st} (A) = B)$
16	11 15	impbid	$⊢ A \in (V \times V) \to (1^{st} (A) = B \leftrightarrow \exists x A = ⟨B, x⟩)$
17	2 16	syl	$⊢ A \in (V \times W) \to (1^{st} (A) = B \leftrightarrow \exists x A = ⟨B, x⟩)$