Theorem 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 \mathrm{V}$$
Assertion	moop2	$$⊢{\exists }^{*}xA=⟨B,x⟩$$

Proof

Step	Hyp	Ref	Expression
1		moop2.1	$$⊢B\in \mathrm{V}$$
2		eqtr2	$$⊢\left(A=⟨B,x⟩\wedge A=⟨⦋y/x⦌B,y⟩\right)\to ⟨B,x⟩=⟨⦋y/x⦌B,y⟩$$
3		vex	$$⊢x\in \mathrm{V}$$
4	1 3	opth	$$⊢⟨B,x⟩=⟨⦋y/x⦌B,y⟩\leftrightarrow \left(B=⦋y/x⦌B\wedge x=y\right)$$
5	4	simprbi	$$⊢⟨B,x⟩=⟨⦋y/x⦌B,y⟩\to x=y$$
6	2 5	syl	$$⊢\left(A=⟨B,x⟩\wedge A=⟨⦋y/x⦌B,y⟩\right)\to x=y$$
7	6	gen2	$$⊢\forall x\forall y\left(\left(A=⟨B,x⟩\wedge A=⟨⦋y/x⦌B,y⟩\right)\to x=y\right)$$
8		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋y/x⦌B$$
9		nfcv	$$⊢\underset{\_}{Ⅎ}xy$$
10	8 9	nfop	$$⊢\underset{\_}{Ⅎ}x⟨⦋y/x⦌B,y⟩$$
11	10	nfeq2	$$⊢ℲxA=⟨⦋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 \left(A=⟨B,x⟩\leftrightarrow A=⟨⦋y/x⦌B,y⟩\right)$$
16	11 15	mo4f	$$⊢{\exists }^{*}xA=⟨B,x⟩\leftrightarrow \forall x\forall y\left(\left(A=⟨B,x⟩\wedge A=⟨⦋y/x⦌B,y⟩\right)\to x=y\right)$$
17	7 16	mpbir	$$⊢{\exists }^{*}xA=⟨B,x⟩$$