Metamath Proof Explorer

Theorem eqvinop

Description: A variable introduction law for ordered pairs. Analogue of Lemma 15 of Monk2 p. 109. (Contributed by NM, 28-May-1995)

		Ref	Expression
	Hypotheses	eqvinop.1	$⊢ B \in V$
		eqvinop.2	$⊢ C \in V$
	Assertion	eqvinop	$⊢ A = ⟨B, C⟩ \leftrightarrow \exists x \exists y (A = ⟨x, y⟩ \land ⟨x, y⟩ = ⟨B, C⟩)$

Proof

Step	Hyp	Ref	Expression
1		eqvinop.1	$⊢ B \in V$
2		eqvinop.2	$⊢ C \in V$
3	1 2	opth2	$⊢ ⟨x, y⟩ = ⟨B, C⟩ \leftrightarrow (x = B \land y = C)$
4	3	anbi2i	$⊢ (A = ⟨x, y⟩ \land ⟨x, y⟩ = ⟨B, C⟩) \leftrightarrow (A = ⟨x, y⟩ \land (x = B \land y = C))$
5		ancom	$⊢ (A = ⟨x, y⟩ \land (x = B \land y = C)) \leftrightarrow ((x = B \land y = C) \land A = ⟨x, y⟩)$
6		anass	$⊢ ((x = B \land y = C) \land A = ⟨x, y⟩) \leftrightarrow (x = B \land (y = C \land A = ⟨x, y⟩))$
7	4 5 6	3bitri	$⊢ (A = ⟨x, y⟩ \land ⟨x, y⟩ = ⟨B, C⟩) \leftrightarrow (x = B \land (y = C \land A = ⟨x, y⟩))$
8	7	exbii	$⊢ \exists y (A = ⟨x, y⟩ \land ⟨x, y⟩ = ⟨B, C⟩) \leftrightarrow \exists y (x = B \land (y = C \land A = ⟨x, y⟩))$
9		19.42v	$⊢ \exists y (x = B \land (y = C \land A = ⟨x, y⟩)) \leftrightarrow (x = B \land \exists y (y = C \land A = ⟨x, y⟩))$
10		opeq2	$⊢ y = C \to ⟨x, y⟩ = ⟨x, C⟩$
11	10	eqeq2d	$⊢ y = C \to (A = ⟨x, y⟩ \leftrightarrow A = ⟨x, C⟩)$
12	2 11	ceqsexv	$⊢ \exists y (y = C \land A = ⟨x, y⟩) \leftrightarrow A = ⟨x, C⟩$
13	12	anbi2i	$⊢ (x = B \land \exists y (y = C \land A = ⟨x, y⟩)) \leftrightarrow (x = B \land A = ⟨x, C⟩)$
14	8 9 13	3bitri	$⊢ \exists y (A = ⟨x, y⟩ \land ⟨x, y⟩ = ⟨B, C⟩) \leftrightarrow (x = B \land A = ⟨x, C⟩)$
15	14	exbii	$⊢ \exists x \exists y (A = ⟨x, y⟩ \land ⟨x, y⟩ = ⟨B, C⟩) \leftrightarrow \exists x (x = B \land A = ⟨x, C⟩)$
16		opeq1	$⊢ x = B \to ⟨x, C⟩ = ⟨B, C⟩$
17	16	eqeq2d	$⊢ x = B \to (A = ⟨x, C⟩ \leftrightarrow A = ⟨B, C⟩)$
18	1 17	ceqsexv	$⊢ \exists x (x = B \land A = ⟨x, C⟩) \leftrightarrow A = ⟨B, C⟩$
19	15 18	bitr2i	$⊢ A = ⟨B, C⟩ \leftrightarrow \exists x \exists y (A = ⟨x, y⟩ \land ⟨x, y⟩ = ⟨B, C⟩)$