moop2

Description: "At most one" property of an ordered pair. (Contributed by NM, 11-Apr-2004) (Revised by Mario Carneiro, 26-Apr-2015)

		Ref	Expression
	Hypothesis	moop2.1	$⊢ B \in V$
	Assertion	moop2	$⊢ \exists^{*} x A = ⟨B, x⟩$

Step	Hyp	Ref	Expression
1		moop2.1	$⊢ B \in V$
2		eqtr2	$⊢ (A = ⟨B, x⟩ \land A = ⟨⦋ y / x ⦌ B, y⟩) \to ⟨B, x⟩ = ⟨⦋ y / x ⦌ B, y⟩$
3		vex	$⊢ x \in V$
4	1 3	opth	$⊢ ⟨B, x⟩ = ⟨⦋ y / x ⦌ B, y⟩ \leftrightarrow (B = ⦋ y / x ⦌ B \land x = y)$
5	4	simprbi	$⊢ ⟨B, x⟩ = ⟨⦋ y / x ⦌ B, y⟩ \to x = y$
6	2 5	syl	$⊢ (A = ⟨B, x⟩ \land A = ⟨⦋ y / x ⦌ B, y⟩) \to x = y$
7	6	gen2	$⊢ \forall x \forall y ((A = ⟨B, x⟩ \land A = ⟨⦋ y / x ⦌ B, y⟩) \to x = y)$
8		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ y / x ⦌ B$
9		nfcv	$⊢ \underline{Ⅎ} x y$
10	8 9	nfop	$⊢ \underline{Ⅎ} x ⟨⦋ y / x ⦌ B, y⟩$
11	10	nfeq2	$⊢ Ⅎ x A = ⟨⦋ y / x ⦌ B, y⟩$
12		csbeq1a	$⊢ x = y \to B = ⦋ y / x ⦌ B$
13		id	$⊢ x = y \to x = y$
14	12 13	opeq12d	$⊢ x = y \to ⟨B, x⟩ = ⟨⦋ y / x ⦌ B, y⟩$
15	14	eqeq2d	$⊢ x = y \to (A = ⟨B, x⟩ \leftrightarrow A = ⟨⦋ y / x ⦌ B, y⟩)$
16	11 15	mo4f	$⊢ \exists^{*} x A = ⟨B, x⟩ \leftrightarrow \forall x \forall y ((A = ⟨B, x⟩ \land A = ⟨⦋ y / x ⦌ B, y⟩) \to x = y)$
17	7 16	mpbir	$⊢ \exists^{*} x A = ⟨B, x⟩$

Metamath Proof Explorer