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

Theorem rmo4 2958
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 2551 . 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 1553 . . . . 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 2548 . . . . 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 2630 . . . . 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 1553 . . 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 2343 . . . . 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 2176 . . 3  |-  ( E* x ( x  e.  A  /\  ph )  <->  A. x A. y ( ( ( x  e.  A  /\  ph )  /\  ( y  e.  A  /\  ps ) )  ->  x  =  y )
)
19 df-ral 2548 . . 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 1527    e. wcel 1684   E*wmo 2144   A.wral 2543   E*wrmo 2546
This theorem is referenced by:  reu4  2959  disjor  4007  somo  4348  supmo  7203  sqrmo  11737  catideu  13577  poslubmo  14250  mgmidmo  14370  lspextmo  15813  evlseu  19400  ply1divmo  19521  cvmliftmo  23815  hilbert1.2  24778  idomsubgmo  27514
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-cleq 2276  df-clel 2279  df-ral 2548  df-rmo 2551
  Copyright terms: Public domain W3C validator