Theorem rmo4 2923

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 2456	. 2 |- ( E* x e. A ph <-> E* x ( x e. A /\ ph ) )
2		an4 581	. . . . . . . . 9 |- ( ( ( x e. A /\ ph ) /\ ( y e. A /\ ps ) ) <-> ( ( x e. A /\ y e. A ) /\ ( ph /\ ps ) ) )
3		ancom 264	. . . . . . . . . 10 |- ( ( x e. A /\ y e. A ) <-> ( y e. A /\ x e. A ) )
4	3	anbi1i 455	. . . . . . . . 9 |- ( ( ( x e. A /\ y e. A ) /\ ( ph /\ ps ) ) <-> ( ( y e. A /\ x e. A ) /\ ( ph /\ ps ) ) )
5	2, 4	bitri 183	. . . . . . . 8 |- ( ( ( x e. A /\ ph ) /\ ( y e. A /\ ps ) ) <-> ( ( y e. A /\ x e. A ) /\ ( ph /\ ps ) ) )
6	5	imbi1i 237	. . . . . . 7 |- ( ( ( ( x e. A /\ ph ) /\ ( y e. A /\ ps ) ) -> x = y ) <-> ( ( ( y e. A /\ x e. A ) /\ ( ph /\ ps ) ) -> x = y ) )
7		impexp 261	. . . . . . 7 |- ( ( ( ( y e. A /\ x e. A ) /\ ( ph /\ ps ) ) -> x = y ) <-> ( ( y e. A /\ x e. A ) -> ( ( ph /\ ps ) -> x = y ) ) )
8		impexp 261	. . . . . . 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 205	. . . . . 6 |- ( ( ( ( x e. A /\ ph ) /\ ( y e. A /\ ps ) ) -> x = y ) <-> ( y e. A -> ( x e. A -> ( ( ph /\ ps ) -> x = y ) ) ) )
10	9	albii 1463	. . . . 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 2453	. . . . 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 2547	. . . . 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 207	. . . 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 1463	. . 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 2233	. . . . 5 |- ( x = y -> ( x e. A <-> y e. A ) )
16		rmo4.1	. . . . 5 |- ( x = y -> ( ph <-> ps ) )
17	15, 16	anbi12d 470	. . . 4 |- ( x = y -> ( ( x e. A /\ ph ) <-> ( y e. A /\ ps ) ) )
18	17	mo4 2080	. . 3 |- ( E* x ( x e. A /\ ph ) <-> A. x A. y ( ( ( x e. A /\ ph ) /\ ( y e. A /\ ps ) ) -> x = y ) )
19		df-ral 2453	. . 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 211	. 2 |- ( E* x ( x e. A /\ ph ) <-> A. x e. A A. y e. A ( ( ph /\ ps ) -> x = y ) )
21	1, 20	bitri 183	1 |- ( E* x e. A ph <-> A. x e. A A. y e. A ( ( ph /\ ps ) -> x = y ) )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104   A.wal 1346   E*wmo 2020   e. wcel 2141   A.wral 2448   E*wrmo 2451

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-cleq 2163  df-clel 2166  df-ral 2453  df-rmo 2456

This theorem is referenced by:  reu4  2924  disjnim  3980  supmoti  6970  lteupri  7579  elrealeu  7791  rereceu  7851  exbtwnz  10207  rsqrmo  10991  divalglemeunn  11880  divalglemeuneg  11882  bezoutlemeu  11962  pw2dvdseu  12122  mgmidmo  12626  mndinvmod  12678  dedekindeu  13395  dedekindicclemicc  13404