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

Theorem rmo4 3264
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 2783 . 2  |-  ( E* x  e.  A  ph  <->  E* x ( x  e.  A  /\  ph )
)
2 an4 831 . . . . . . . . 9  |-  ( ( ( x  e.  A  /\  ph )  /\  (
y  e.  A  /\  ps ) )  <->  ( (
x  e.  A  /\  y  e.  A )  /\  ( ph  /\  ps ) ) )
3 ancom 451 . . . . . . . . . 10  |-  ( ( x  e.  A  /\  y  e.  A )  <->  ( y  e.  A  /\  x  e.  A )
)
43anbi1i 699 . . . . . . . . 9  |-  ( ( ( x  e.  A  /\  y  e.  A
)  /\  ( ph  /\ 
ps ) )  <->  ( (
y  e.  A  /\  x  e.  A )  /\  ( ph  /\  ps ) ) )
52, 4bitri 252 . . . . . . . 8  |-  ( ( ( x  e.  A  /\  ph )  /\  (
y  e.  A  /\  ps ) )  <->  ( (
y  e.  A  /\  x  e.  A )  /\  ( ph  /\  ps ) ) )
65imbi1i 326 . . . . . . 7  |-  ( ( ( ( x  e.  A  /\  ph )  /\  ( y  e.  A  /\  ps ) )  ->  x  =  y )  <->  ( ( ( y  e.  A  /\  x  e.  A )  /\  ( ph  /\  ps ) )  ->  x  =  y ) )
7 impexp 447 . . . . . . 7  |-  ( ( ( ( y  e.  A  /\  x  e.  A )  /\  ( ph  /\  ps ) )  ->  x  =  y )  <->  ( ( y  e.  A  /\  x  e.  A )  ->  (
( ph  /\  ps )  ->  x  =  y ) ) )
8 impexp 447 . . . . . . 7  |-  ( ( ( y  e.  A  /\  x  e.  A
)  ->  ( ( ph  /\  ps )  ->  x  =  y )
)  <->  ( y  e.  A  ->  ( x  e.  A  ->  ( (
ph  /\  ps )  ->  x  =  y ) ) ) )
96, 7, 83bitri 274 . . . . . 6  |-  ( ( ( ( x  e.  A  /\  ph )  /\  ( y  e.  A  /\  ps ) )  ->  x  =  y )  <->  ( y  e.  A  -> 
( x  e.  A  ->  ( ( ph  /\  ps )  ->  x  =  y ) ) ) )
109albii 1687 . . . . 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 2780 . . . . 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 2830 . . . . 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 276 . . . 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 1687 . . 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 2494 . . . . 5  |-  ( x  =  y  ->  (
x  e.  A  <->  y  e.  A ) )
16 rmo4.1 . . . . 5  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
1715, 16anbi12d 715 . . . 4  |-  ( x  =  y  ->  (
( x  e.  A  /\  ph )  <->  ( y  e.  A  /\  ps )
) )
1817mo4 2313 . . 3  |-  ( E* x ( x  e.  A  /\  ph )  <->  A. x A. y ( ( ( x  e.  A  /\  ph )  /\  ( y  e.  A  /\  ps ) )  ->  x  =  y )
)
19 df-ral 2780 . . 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 280 . 2  |-  ( E* x ( x  e.  A  /\  ph )  <->  A. x  e.  A  A. y  e.  A  (
( ph  /\  ps )  ->  x  =  y ) )
211, 20bitri 252 1  |-  ( E* x  e.  A  ph  <->  A. x  e.  A  A. y  e.  A  (
( ph  /\  ps )  ->  x  =  y ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370   A.wal 1435    e. wcel 1868   E*wmo 2266   A.wral 2775   E*wrmo 2778
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-cleq 2414  df-clel 2417  df-ral 2780  df-rmo 2783
This theorem is referenced by:  reu4  3265  disjor  4405  somo  4804  supmo  7968  infmo  8013  sqrmo  13303  catideu  15568  poslubmo  16379  posglbmo  16380  mgmidmo  16489  lspextmo  18266  evlseu  18726  ply1divmo  23072  tghilberti2  24669  foot  24750  mideu  24766  2sqmo  28404  cvmliftmo  30002  hilbert1.2  30914  poimirlem1  31854  poimirlem13  31866  poimirlem14  31867  poimirlem18  31871  poimirlem21  31874  idomsubgmo  35991
  Copyright terms: Public domain W3C validator