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

Theorem ralnex 2638
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 2633 . 2  |-  ( A. x  e.  A  -.  ph  <->  A. x ( x  e.  A  ->  -.  ph )
)
2 alinexa 1583 . . 3  |-  ( A. x ( x  e.  A  ->  -.  ph )  <->  -. 
E. x ( x  e.  A  /\  ph ) )
3 df-rex 2634 . . 3  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
42, 3xchbinxr 302 . 2  |-  ( A. x ( x  e.  A  ->  -.  ph )  <->  -. 
E. x  e.  A  ph )
51, 4bitri 240 1  |-  ( A. x  e.  A  -.  ph  <->  -. 
E. x  e.  A  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    /\ wa 358   A.wal 1545   E.wex 1546    e. wcel 1715   A.wral 2628   E.wrex 2629
This theorem is referenced by:  dfrex2  2641  ralinexa  2673  nrex  2730  nrexdv  2731  r19.43  2780  rabeq0  3564  iindif2  4073  ordunisuc2  4738  tfi  4747  rexiunxp  4929  rexxpf  4934  omeulem1  6722  frfi  7249  isfinite2  7262  dfsup2OLD  7343  supmo  7350  ordtypelem9  7388  elirrv  7458  unbndrank  7661  kmlem7  7929  kmlem8  7930  kmlem13  7935  isfin1-3  8159  ac6num  8253  ac9  8257  ac9s  8267  zorn2lem4  8273  fpwwe2lem12  8410  npomex  8767  genpnnp  8776  suplem2pr  8824  suprnub  9864  infmrgelb  9881  arch  10111  xrsupsslem  10778  xrinfmsslem  10779  supxrbnd1  10793  supxrbnd2  10794  supxrleub  10798  supxrbnd  10800  infmxrgelb  10806  injresinjlem  11086  hashgt12el  11569  hashgt12el2  11570  sqr2irr  12735  prmind2  12977  vdwnnlem3  13252  vdwnn  13253  acsfiindd  14490  isnirred  15692  lssne0  15918  t1conperf  17379  trfbas  17752  fbunfip  17777  fbasrn  17792  filuni  17793  hausflim  17889  alexsubALTlem3  17956  alexsubALTlem4  17957  ptcmplem4  17962  lebnumlem3  18676  bcthlem4  18964  bcth3  18968  amgm  20507  issqf  20597  ostth  21011  usgranloop0  21077  nmounbi  21667  lnon0  21689  largei  23160  cvbr2  23176  chrelat2i  23258  lmdvg  23693  ballotlemimin  24211  dedekind  24671  dfon2lem8  24887  axcontlem12  25345  heiborlem1  26041  rencldnfilem  26409  setindtr  26623  stirlinglem5  27333  vdusgra0nedg  27818  usgravd0nedg  27822  frgra2v  27834  bnj110  28654  bnj1417  28835  lcvbr2  29283  lcvbr3  29284  cvrnbtwn  29532  cvrval2  29535  hlrelat2  29663  cdleme0nex  30550
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1547  df-ral 2633  df-rex 2634
  Copyright terms: Public domain W3C validator