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 e. _V
Assertion	moop2	|- E* x A = <. B , x >.

Proof

Step	Hyp	Ref	Expression
1		moop2.1	|- B e. _V
2		eqtr2	|- ( ( A = <. B , x >. /\ A = <. [_ y / x ]_ B , y >. ) -> <. B , x >. = <. [_ y / x ]_ B , y >. )
3		vex	|- x e. _V
4	1 3	opth	|- ( <. B , x >. = <. [_ y / x ]_ B , y >. <-> ( B = [_ y / x ]_ B /\ x = y ) )
5	4	simprbi	|- ( <. B , x >. = <. [_ y / x ]_ B , y >. -> x = y )
6	2 5	syl	|- ( ( A = <. B , x >. /\ A = <. [_ y / x ]_ B , y >. ) -> x = y )
7	6	gen2	|- A. x A. y ( ( A = <. B , x >. /\ A = <. [_ y / x ]_ B , y >. ) -> x = y )
8		nfcsb1v	|- F/_ x [_ y / x ]_ B
9		nfcv	|- F/_ x y
10	8 9	nfop	|- F/_ x <. [_ y / x ]_ B , y >.
11	10	nfeq2	|- F/ x A = <. [_ y / x ]_ B , y >.
12		csbeq1a	|- ( x = y -> B = [_ y / x ]_ B )
13		id	|- ( x = y -> x = y )
14	12 13	opeq12d	|- ( x = y -> <. B , x >. = <. [_ y / x ]_ B , y >. )
15	14	eqeq2d	|- ( x = y -> ( A = <. B , x >. <-> A = <. [_ y / x ]_ B , y >. ) )
16	11 15	mo4f	|- ( E* x A = <. B , x >. <-> A. x A. y ( ( A = <. B , x >. /\ A = <. [_ y / x ]_ B , y >. ) -> x = y ) )
17	7 16	mpbir	|- E* x A = <. B , x >.