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

Theorem ralnex 2717
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 2712 . 2  |-  ( A. x  e.  A  -.  ph  <->  A. x ( x  e.  A  ->  -.  ph )
)
2 alinexa 1589 . . 3  |-  ( A. x ( x  e.  A  ->  -.  ph )  <->  -. 
E. x ( x  e.  A  /\  ph ) )
3 df-rex 2713 . . 3  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
42, 3xchbinxr 304 . 2  |-  ( A. x ( x  e.  A  ->  -.  ph )  <->  -. 
E. x  e.  A  ph )
51, 4bitri 242 1  |-  ( A. x  e.  A  -.  ph  <->  -. 
E. x  e.  A  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 178    /\ wa 360   A.wal 1550   E.wex 1551    e. wcel 1726   A.wral 2707   E.wrex 2708
This theorem is referenced by:  dfrex2  2720  ralinexa  2752  nrexralim  2754  nrex  2810  nrexdv  2811  r19.43  2865  rabeq0  3651  iindif2  4162  ordunisuc2  4827  tfi  4836  rexiunxp  5018  rexxpf  5023  omeulem1  6828  frfi  7355  isfinite2  7368  dfsup2OLD  7451  supmo  7460  ordtypelem9  7498  elirrv  7568  unbndrank  7771  kmlem7  8041  kmlem8  8042  kmlem13  8047  isfin1-3  8271  ac6num  8364  zorn2lem4  8384  fpwwe2lem12  8521  npomex  8878  genpnnp  8887  suplem2pr  8935  suprnub  9976  infmrgelb  9993  arch  10223  xrsupsslem  10890  xrinfmsslem  10891  supxrbnd1  10905  supxrbnd2  10906  supxrleub  10910  supxrbnd  10912  infmxrgelb  10918  injresinjlem  11204  hashgt12el  11687  hashgt12el2  11688  sqr2irr  12853  prmind2  13095  vdwnnlem3  13370  vdwnn  13371  acsfiindd  14608  isnirred  15810  lssne0  16032  t1conperf  17504  trfbas  17881  fbunfip  17906  fbasrn  17921  filuni  17922  hausflim  18018  alexsubALTlem3  18085  alexsubALTlem4  18086  ptcmplem4  18091  lebnumlem3  18993  bcthlem4  19285  bcth3  19289  amgm  20834  issqf  20924  ostth  21338  usgranloop0  21405  vdusgra0nedg  21684  usgravd0nedg  21688  nmounbi  22282  lnon0  22304  largei  23775  cvbr2  23791  chrelat2i  23873  toslub  24196  tosglb  24197  lmdvg  24343  dedekind  25192  dfon2lem8  25422  dfint3  25802  axcontlem12  25919  mblfinlem1  26255  ftc1anc  26302  heiborlem1  26534  rencldnfilem  26895  setindtr  27109  stirlinglem5  27817  otiunsndisjX  28082  f0rn0  28093  usgravd00  28436  frgra2v  28463  2spotiundisj  28525  2spot0  28527  bnj110  29303  bnj1417  29484  lcvbr2  29894  lcvbr3  29895  cvrnbtwn  30143  cvrval2  30146  hlrelat2  30274  cdleme0nex  31161
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-ral 2712  df-rex 2713
  Copyright terms: Public domain W3C validator