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

Theorem ralnex 2991
Description: Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.) (Proof shortened by BJ, 16-Jul-2021.)
Assertion
Ref Expression
ralnex (∀𝑥𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥𝐴 𝜑)

Proof of Theorem ralnex
StepHypRef Expression
1 raln 2990 . 2 (∀𝑥𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥𝐴𝜑))
2 alnex 1705 . . 3 (∀𝑥 ¬ (𝑥𝐴𝜑) ↔ ¬ ∃𝑥(𝑥𝐴𝜑))
3 df-rex 2917 . . 3 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
42, 3xchbinxr 325 . 2 (∀𝑥 ¬ (𝑥𝐴𝜑) ↔ ¬ ∃𝑥𝐴 𝜑)
51, 4bitri 264 1 (∀𝑥𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196  wa 384  wal 1480  wex 1703  wcel 1989  wral 2911  wrex 2912
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1704  df-ral 2916  df-rex 2917
This theorem is referenced by:  dfral2  2993  dfrex2  2995  ralinexa  2996  nrexralim  2998  nrex  2999  nrexdv  3000  r19.43  3091  rabeq0OLD  3958  n0snor2el  4362  iindif2  4587  rexiunxp  5260  rexxpf  5267  f0rn0  6088  ordunisuc2  7041  tfi  7050  omeulem1  7659  frfi  8202  isfinite2  8215  supmo  8355  infmo  8398  ordtypelem9  8428  elirrv  8501  unbndrank  8702  kmlem7  8975  kmlem8  8976  kmlem13  8981  isfin1-3  9205  ac6num  9298  zorn2lem4  9318  fpwwe2lem12  9460  npomex  9815  genpnnp  9824  suplem2pr  9872  dedekind  10197  suprnub  10985  infregelb  11004  arch  11286  xrsupsslem  12134  xrinfmsslem  12135  supxrbnd1  12148  supxrbnd2  12149  supxrleub  12153  supxrbnd  12155  infxrgelb  12162  injresinjlem  12583  hashgt12el  13205  hashgt12el2  13206  sqrt2irr  14973  prmind2  15392  vdwnnlem3  15695  vdwnn  15696  acsfiindd  17171  isnmnd  17292  isnirred  18694  lssne0  18945  bwth  21207  t1connperf  21233  trfbas  21642  fbunfip  21667  fbasrn  21682  filuni  21683  hausflim  21779  alexsubALTlem3  21847  alexsubALTlem4  21848  ptcmplem4  21853  lebnumlem3  22756  bcthlem4  23118  bcth3  23122  amgm  24711  issqf  24856  ostth  25322  tglowdim2ln  25540  axcontlem12  25849  umgrnloop0  25998  numedglnl  26033  usgrnloop0ALT  26091  uhgrnbgr0nb  26244  nbgr0edg  26247  vtxd0nedgb  26378  vtxdusgr0edgnelALT  26386  1hevtxdg0  26395  usgrvd0nedg  26423  uhgrvd00  26424  pthdlem2lem  26657  nmounbi  27615  lnon0  27637  largei  29110  cvbr2  29126  chrelat2i  29208  uniinn0  29350  infxrge0gelb  29516  nn0min  29552  toslublem  29652  tosglblem  29654  archiabl  29737  lmdvg  29984  esumcvgre  30138  eulerpartlems  30407  bnj110  30913  bnj1417  31094  dfon2lem8  31679  nosupbnd1lem4  31841  sltrec  31908  dfint3  32043  unblimceq0  32482  relowlpssretop  33192  poimirlem26  33415  poimirlem30  33419  poimir  33422  mblfinlem1  33426  ftc1anc  33473  heiborlem1  33590  lcvbr2  34135  lcvbr3  34136  cvrnbtwn  34384  cvrval2  34387  hlrelat2  34515  cdleme0nex  35403  rencldnfilem  37210  setindtr  37417  gneispace  38258  nelrnmpt  39083  supxrgere  39368  supxrgelem  39372  infxrbnd2  39404  supminfxr  39513  limsupub  39742  limsuppnflem  39748  limsupre2lem  39762  stirlinglem5  40064  etransclem24  40244  etransclem32  40252  sge0iunmpt  40404  sge0rpcpnf  40407  iundjiun  40446  voliunsge0lem  40458  meaiininclem  40469  hoidmv1lelem3  40576  hoidmvlelem4  40581  hoidmvlelem5  40582  copisnmnd  41580  lindslinindsimp1  42017  lindslinindsimp2  42023  ldepslinc  42069  aacllem  42318
  Copyright terms: Public domain W3C validator