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

Theorem ralnex 2553
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 2548 . 2  |-  ( A. x  e.  A  -.  ph  <->  A. x ( x  e.  A  ->  -.  ph )
)
2 alinexa 1565 . . 3  |-  ( A. x ( x  e.  A  ->  -.  ph )  <->  -. 
E. x ( x  e.  A  /\  ph ) )
3 df-rex 2549 . . 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 1527   E.wex 1528    e. wcel 1684   A.wral 2543   E.wrex 2544
This theorem is referenced by:  dfrex2  2556  ralinexa  2588  nrex  2645  nrexdv  2646  r19.43  2695  rabeq0  3476  iindif2  3971  ordunisuc2  4635  tfi  4644  rexiunxp  4826  rexxpf  4831  omeulem1  6580  frfi  7102  isfinite2  7115  dfsup2OLD  7196  supmo  7203  ordtypelem9  7241  elirrv  7311  unbndrank  7514  kmlem7  7782  kmlem8  7783  kmlem13  7788  isfin1-3  8012  ac6num  8106  ac9  8110  ac9s  8120  zorn2lem4  8126  fpwwe2lem12  8263  npomex  8620  genpnnp  8629  suplem2pr  8677  suprnub  9717  infmrgelb  9734  arch  9962  xrsupsslem  10625  xrinfmsslem  10626  supxrbnd1  10640  supxrbnd2  10641  supxrleub  10645  supxrbnd  10647  infmxrgelb  10653  sqr2irr  12527  prmind2  12769  vdwnnlem3  13044  vdwnn  13045  acsfiindd  14280  isnirred  15482  lssne0  15708  t1conperf  17162  trfbas  17539  fbunfip  17564  fbasrn  17579  filuni  17580  hausflim  17676  alexsubALTlem3  17743  alexsubALTlem4  17744  ptcmplem4  17749  lebnumlem3  18461  bcthlem4  18749  bcth3  18753  amgm  20285  issqf  20374  ostth  20788  nmounbi  21354  lnon0  21376  largei  22847  cvbr2  22863  chrelat2i  22945  ballotlemimin  23064  lmdvg  23376  dedekind  24082  dfon2lem8  24146  axcontlem12  24603  negcmpprcal1  24945  negcmpprcal2  24946  dstr  25171  lvsovso2  25627  bsstrs  26146  nbssntrs  26147  heiborlem1  26535  rencldnfilem  26903  setindtr  27117  stirlinglem5  27827  frgra2v  28177  bnj110  28890  bnj1417  29071  lcvbr2  29212  lcvbr3  29213  cvrnbtwn  29461  cvrval2  29464  hlrelat2  29592  cdleme0nex  30479
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-ral 2548  df-rex 2549
  Copyright terms: Public domain W3C validator