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

Theorem ralnex 2684
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 2679 . 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 2680 . . 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 2674   E.wrex 2675
This theorem is referenced by:  dfrex2  2687  ralinexa  2719  nrex  2776  nrexdv  2777  r19.43  2831  rabeq0  3617  iindif2  4128  ordunisuc2  4791  tfi  4800  rexiunxp  4982  rexxpf  4987  omeulem1  6792  frfi  7319  isfinite2  7332  dfsup2OLD  7414  supmo  7421  ordtypelem9  7459  elirrv  7529  unbndrank  7732  kmlem7  8000  kmlem8  8001  kmlem13  8006  isfin1-3  8230  ac6num  8323  zorn2lem4  8343  fpwwe2lem12  8480  npomex  8837  genpnnp  8846  suplem2pr  8894  suprnub  9935  infmrgelb  9952  arch  10182  xrsupsslem  10849  xrinfmsslem  10850  supxrbnd1  10864  supxrbnd2  10865  supxrleub  10869  supxrbnd  10871  infmxrgelb  10877  injresinjlem  11162  hashgt12el  11645  hashgt12el2  11646  sqr2irr  12811  prmind2  13053  vdwnnlem3  13328  vdwnn  13329  acsfiindd  14566  isnirred  15768  lssne0  15990  t1conperf  17460  trfbas  17837  fbunfip  17862  fbasrn  17877  filuni  17878  hausflim  17974  alexsubALTlem3  18041  alexsubALTlem4  18042  ptcmplem4  18047  lebnumlem3  18949  bcthlem4  19241  bcth3  19245  amgm  20790  issqf  20880  ostth  21294  usgranloop0  21361  vdusgra0nedg  21640  usgravd0nedg  21644  nmounbi  22238  lnon0  22260  largei  23731  cvbr2  23747  chrelat2i  23829  toslub  24152  tosglb  24153  lmdvg  24299  dedekind  25148  dfon2lem8  25368  axcontlem12  25826  mblfinlem  26151  heiborlem1  26418  rencldnfilem  26779  setindtr  26993  stirlinglem5  27702  otiunsndisjX  27963  frgra2v  28111  2spotiundisj  28173  2spot0  28175  bnj110  28947  bnj1417  29128  lcvbr2  29517  lcvbr3  29518  cvrnbtwn  29766  cvrval2  29769  hlrelat2  29897  cdleme0nex  30784
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 2679  df-rex 2680
  Copyright terms: Public domain W3C validator