Theorem rmo4 2930

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 2463	. 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 1470	. . . . 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 2460	. . . . 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 2554	. . . . 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 1470	. . 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 2240	. . . . 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 2087	. . 3 |- ( E* x ( x e. A /\ ph ) <-> A. x A. y ( ( ( x e. A /\ ph ) /\ ( y e. A /\ ps ) ) -> x = y ) )
19		df-ral 2460	. . 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 1351   E*wmo 2027   e. wcel 2148   A.wral 2455   E*wrmo 2458

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-cleq 2170  df-clel 2173  df-ral 2460  df-rmo 2463

This theorem is referenced by:  reu4  2931  disjnim  3994  supmoti  6991  lteupri  7615  elrealeu  7827  rereceu  7887  exbtwnz  10250  rsqrmo  11035  divalglemeunn  11925  divalglemeuneg  11927  bezoutlemeu  12007  pw2dvdseu  12167  mgmidmo  12790  mndinvmod  12845  dedekindeu  14071  dedekindicclemicc  14080