Theorem rmo4 2942

Description: Restricted "at most one" using implicit substitution. (Contributed by NM, 24-Oct-2006.) (Revised by NM, 16-Jun-2017.)

Hypothesis

Ref	Expression
rmo4.1	|- ( x = y -> ( ph <-> ps ) )

Assertion

Ref	Expression
rmo4	|- ( E* x e. A ph <-> A. x e. A A. y e. A ( ( ph /\ ps ) -> x = y ) )

Distinct variable groups:   x, y, A   ph, y   ps, x

Allowed substitution hints:   ph( x)   ps( y)

Proof of Theorem rmo4

Step	Hyp	Ref	Expression
1		df-rmo 2473	. 2 |- ( E* x e. A ph <-> E* x ( x e. A /\ ph ) )
2		an4 586	. . . . . . . . 9 |- ( ( ( x e. A /\ ph ) /\ ( y e. A /\ ps ) ) <-> ( ( x e. A /\ y e. A ) /\ ( ph /\ ps ) ) )
3		ancom 266	. . . . . . . . . 10 |- ( ( x e. A /\ y e. A ) <-> ( y e. A /\ x e. A ) )
4	3	anbi1i 458	. . . . . . . . 9 |- ( ( ( x e. A /\ y e. A ) /\ ( ph /\ ps ) ) <-> ( ( y e. A /\ x e. A ) /\ ( ph /\ ps ) ) )
5	2, 4	bitri 184	. . . . . . . 8 |- ( ( ( x e. A /\ ph ) /\ ( y e. A /\ ps ) ) <-> ( ( y e. A /\ x e. A ) /\ ( ph /\ ps ) ) )
6	5	imbi1i 238	. . . . . . 7 |- ( ( ( ( x e. A /\ ph ) /\ ( y e. A /\ ps ) ) -> x = y ) <-> ( ( ( y e. A /\ x e. A ) /\ ( ph /\ ps ) ) -> x = y ) )
7		impexp 263	. . . . . . 7 |- ( ( ( ( y e. A /\ x e. A ) /\ ( ph /\ ps ) ) -> x = y ) <-> ( ( y e. A /\ x e. A ) -> ( ( ph /\ ps ) -> x = y ) ) )
8		impexp 263	. . . . . . 7 |- ( ( ( y e. A /\ x e. A ) -> ( ( ph /\ ps ) -> x = y ) ) <-> ( y e. A -> ( x e. A -> ( ( ph /\ ps ) -> x = y ) ) ) )
9	6, 7, 8	3bitri 206	. . . . . 6 |- ( ( ( ( x e. A /\ ph ) /\ ( y e. A /\ ps ) ) -> x = y ) <-> ( y e. A -> ( x e. A -> ( ( ph /\ ps ) -> x = y ) ) ) )
10	9	albii 1480	. . . . 5 |- ( A. y ( ( ( x e. A /\ ph ) /\ ( y e. A /\ ps ) ) -> x = y ) <-> A. y ( y e. A -> ( x e. A -> ( ( ph /\ ps ) -> x = y ) ) ) )
11		df-ral 2470	. . . . 5 |- ( A. y e. A ( x e. A -> ( ( ph /\ ps ) -> x = y ) ) <-> A. y ( y e. A -> ( x e. A -> ( ( ph /\ ps ) -> x = y ) ) ) )
12		r19.21v 2564	. . . . 5 |- ( A. y e. A ( x e. A -> ( ( ph /\ ps ) -> x = y ) ) <-> ( x e. A -> A. y e. A ( ( ph /\ ps ) -> x = y ) ) )
13	10, 11, 12	3bitr2i 208	. . . 4 |- ( A. y ( ( ( x e. A /\ ph ) /\ ( y e. A /\ ps ) ) -> x = y ) <-> ( x e. A -> A. y e. A ( ( ph /\ ps ) -> x = y ) ) )
14	13	albii 1480	. . 3 |- ( A. x A. y ( ( ( x e. A /\ ph ) /\ ( y e. A /\ ps ) ) -> x = y ) <-> A. x ( x e. A -> A. y e. A ( ( ph /\ ps ) -> x = y ) ) )
15		eleq1 2250	. . . . 5 |- ( x = y -> ( x e. A <-> y e. A ) )
16		rmo4.1	. . . . 5 |- ( x = y -> ( ph <-> ps ) )
17	15, 16	anbi12d 473	. . . 4 |- ( x = y -> ( ( x e. A /\ ph ) <-> ( y e. A /\ ps ) ) )
18	17	mo4 2097	. . 3 |- ( E* x ( x e. A /\ ph ) <-> A. x A. y ( ( ( x e. A /\ ph ) /\ ( y e. A /\ ps ) ) -> x = y ) )
19		df-ral 2470	. . 3 |- ( A. x e. A A. y e. A ( ( ph /\ ps ) -> x = y ) <-> A. x ( x e. A -> A. y e. A ( ( ph /\ ps ) -> x = y ) ) )
20	14, 18, 19	3bitr4i 212	. 2 |- ( E* x ( x e. A /\ ph ) <-> A. x e. A A. y e. A ( ( ph /\ ps ) -> x = y ) )
21	1, 20	bitri 184	1 |- ( E* x e. A ph <-> A. x e. A A. y e. A ( ( ph /\ ps ) -> x = y ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   A.wal 1361   E*wmo 2037   e. wcel 2158   A.wral 2465   E*wrmo 2468

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-nf 1471  df-sb 1773  df-eu 2039  df-mo 2040  df-cleq 2180  df-clel 2183  df-ral 2470  df-rmo 2473

This theorem is referenced by:  reu4  2943  disjnim  4006  supmoti  7005  lteupri  7629  elrealeu  7841  rereceu  7901  exbtwnz  10264  rsqrmo  11049  divalglemeunn  11939  divalglemeuneg  11941  bezoutlemeu  12021  pw2dvdseu  12181  mgmidmo  12809  mndinvmod  12867  dedekindeu  14372  dedekindicclemicc  14381