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

Theorem ralnex 2676
Description: Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.)
Assertion
Ref Expression
ralnex  |-  ( A. x  e.  A  -.  ph  <->  -. 
E. x  e.  A  ph )

Proof of Theorem ralnex
StepHypRef Expression
1 df-ral 2671 . 2  |-  ( A. x  e.  A  -.  ph  <->  A. x ( x  e.  A  ->  -.  ph )
)
2 alinexa 1585 . . 3  |-  ( A. x ( x  e.  A  ->  -.  ph )  <->  -. 
E. x ( x  e.  A  /\  ph ) )
3 df-rex 2672 . . 3  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
42, 3xchbinxr 303 . 2  |-  ( A. x ( x  e.  A  ->  -.  ph )  <->  -. 
E. x  e.  A  ph )
51, 4bitri 241 1  |-  ( A. x  e.  A  -.  ph  <->  -. 
E. x  e.  A  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    /\ wa 359   A.wal 1546   E.wex 1547    e. wcel 1721   A.wral 2666   E.wrex 2667
This theorem is referenced by:  dfrex2  2679  ralinexa  2711  nrex  2768  nrexdv  2769  r19.43  2823  rabeq0  3609  iindif2  4120  ordunisuc2  4783  tfi  4792  rexiunxp  4974  rexxpf  4979  omeulem1  6784  frfi  7311  isfinite2  7324  dfsup2OLD  7406  supmo  7413  ordtypelem9  7451  elirrv  7521  unbndrank  7724  kmlem7  7992  kmlem8  7993  kmlem13  7998  isfin1-3  8222  ac6num  8315  zorn2lem4  8335  fpwwe2lem12  8472  npomex  8829  genpnnp  8838  suplem2pr  8886  suprnub  9927  infmrgelb  9944  arch  10174  xrsupsslem  10841  xrinfmsslem  10842  supxrbnd1  10856  supxrbnd2  10857  supxrleub  10861  supxrbnd  10863  infmxrgelb  10869  injresinjlem  11154  hashgt12el  11637  hashgt12el2  11638  sqr2irr  12803  prmind2  13045  vdwnnlem3  13320  vdwnn  13321  acsfiindd  14558  isnirred  15760  lssne0  15982  t1conperf  17452  trfbas  17829  fbunfip  17854  fbasrn  17869  filuni  17870  hausflim  17966  alexsubALTlem3  18033  alexsubALTlem4  18034  ptcmplem4  18039  lebnumlem3  18941  bcthlem4  19233  bcth3  19237  amgm  20782  issqf  20872  ostth  21286  usgranloop0  21353  vdusgra0nedg  21632  usgravd0nedg  21636  nmounbi  22230  lnon0  22252  largei  23723  cvbr2  23739  chrelat2i  23821  toslub  24144  tosglb  24145  lmdvg  24291  dedekind  25140  dfon2lem8  25360  axcontlem12  25818  mblfinlem  26143  heiborlem1  26410  rencldnfilem  26771  setindtr  26985  stirlinglem5  27694  otiunsndisjX  27955  frgra2v  28103  2spotiundisj  28165  2spot0  28167  bnj110  28935  bnj1417  29116  lcvbr2  29505  lcvbr3  29506  cvrnbtwn  29754  cvrval2  29757  hlrelat2  29885  cdleme0nex  30772
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-ral 2671  df-rex 2672
  Copyright terms: Public domain W3C validator