MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rmo4 Unicode version

Theorem rmo4 2971
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
StepHypRef Expression
1 df-rmo 2564 . 2  |-  ( E* x  e.  A ph  <->  E* x ( x  e.  A  /\  ph )
)
2 an4 797 . . . . . . . . 9  |-  ( ( ( x  e.  A  /\  ph )  /\  (
y  e.  A  /\  ps ) )  <->  ( (
x  e.  A  /\  y  e.  A )  /\  ( ph  /\  ps ) ) )
3 ancom 437 . . . . . . . . . 10  |-  ( ( x  e.  A  /\  y  e.  A )  <->  ( y  e.  A  /\  x  e.  A )
)
43anbi1i 676 . . . . . . . . 9  |-  ( ( ( x  e.  A  /\  y  e.  A
)  /\  ( ph  /\ 
ps ) )  <->  ( (
y  e.  A  /\  x  e.  A )  /\  ( ph  /\  ps ) ) )
52, 4bitri 240 . . . . . . . 8  |-  ( ( ( x  e.  A  /\  ph )  /\  (
y  e.  A  /\  ps ) )  <->  ( (
y  e.  A  /\  x  e.  A )  /\  ( ph  /\  ps ) ) )
65imbi1i 315 . . . . . . 7  |-  ( ( ( ( x  e.  A  /\  ph )  /\  ( y  e.  A  /\  ps ) )  ->  x  =  y )  <->  ( ( ( y  e.  A  /\  x  e.  A )  /\  ( ph  /\  ps ) )  ->  x  =  y ) )
7 impexp 433 . . . . . . 7  |-  ( ( ( ( y  e.  A  /\  x  e.  A )  /\  ( ph  /\  ps ) )  ->  x  =  y )  <->  ( ( y  e.  A  /\  x  e.  A )  ->  (
( ph  /\  ps )  ->  x  =  y ) ) )
8 impexp 433 . . . . . . 7  |-  ( ( ( y  e.  A  /\  x  e.  A
)  ->  ( ( ph  /\  ps )  ->  x  =  y )
)  <->  ( y  e.  A  ->  ( x  e.  A  ->  ( (
ph  /\  ps )  ->  x  =  y ) ) ) )
96, 7, 83bitri 262 . . . . . 6  |-  ( ( ( ( x  e.  A  /\  ph )  /\  ( y  e.  A  /\  ps ) )  ->  x  =  y )  <->  ( y  e.  A  -> 
( x  e.  A  ->  ( ( ph  /\  ps )  ->  x  =  y ) ) ) )
109albii 1556 . . . . 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 2561 . . . . 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 2643 . . . . 5  |-  ( A. y  e.  A  (
x  e.  A  -> 
( ( ph  /\  ps )  ->  x  =  y ) )  <->  ( x  e.  A  ->  A. y  e.  A  ( ( ph  /\  ps )  ->  x  =  y )
) )
1310, 11, 123bitr2i 264 . . . 4  |-  ( A. y ( ( ( x  e.  A  /\  ph )  /\  ( y  e.  A  /\  ps ) )  ->  x  =  y )  <->  ( x  e.  A  ->  A. y  e.  A  ( ( ph  /\  ps )  ->  x  =  y )
) )
1413albii 1556 . . 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 2356 . . . . 5  |-  ( x  =  y  ->  (
x  e.  A  <->  y  e.  A ) )
16 rmo4.1 . . . . 5  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
1715, 16anbi12d 691 . . . 4  |-  ( x  =  y  ->  (
( x  e.  A  /\  ph )  <->  ( y  e.  A  /\  ps )
) )
1817mo4 2189 . . 3  |-  ( E* x ( x  e.  A  /\  ph )  <->  A. x A. y ( ( ( x  e.  A  /\  ph )  /\  ( y  e.  A  /\  ps ) )  ->  x  =  y )
)
19 df-ral 2561 . . 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 )
) )
2014, 18, 193bitr4i 268 . 2  |-  ( E* x ( x  e.  A  /\  ph )  <->  A. x  e.  A  A. y  e.  A  (
( ph  /\  ps )  ->  x  =  y ) )
211, 20bitri 240 1  |-  ( E* x  e.  A ph  <->  A. x  e.  A  A. y  e.  A  (
( ph  /\  ps )  ->  x  =  y ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358   A.wal 1530    e. wcel 1696   E*wmo 2157   A.wral 2556   E*wrmo 2559
This theorem is referenced by:  reu4  2972  disjor  4023  somo  4364  supmo  7219  sqrmo  11753  catideu  13593  poslubmo  14266  mgmidmo  14386  lspextmo  15829  evlseu  19416  ply1divmo  19537  cvmliftmo  23830  hilbert1.2  24850  idomsubgmo  27617
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-cleq 2289  df-clel 2292  df-ral 2561  df-rmo 2564
  Copyright terms: Public domain W3C validator