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

Theorem ralnex 3021
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 3020 . 2 (∀𝑥𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥𝐴𝜑))
2 alnex 1746 . . 3 (∀𝑥 ¬ (𝑥𝐴𝜑) ↔ ¬ ∃𝑥(𝑥𝐴𝜑))
3 df-rex 2947 . . 3 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
42, 3xchbinxr 324 . 2 (∀𝑥 ¬ (𝑥𝐴𝜑) ↔ ¬ ∃𝑥𝐴 𝜑)
51, 4bitri 264 1 (∀𝑥𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196  wa 383  wal 1521  wex 1744  wcel 2030  wral 2941  wrex 2942
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-ral 2946  df-rex 2947
This theorem is referenced by:  dfral2  3023  dfrex2  3025  ralinexa  3026  nrexralim  3028  nrex  3029  nrexdv  3030  r19.43  3122  rabeq0OLD  3993  n0snor2el  4396  iindif2  4621  rexiunxp  5295  rexxpf  5302  f0rn0  6128  ordunisuc2  7086  tfi  7095  omeulem1  7707  frfi  8246  isfinite2  8259  supmo  8399  infmo  8442  ordtypelem9  8472  elirrv  8542  unbndrank  8743  kmlem7  9016  kmlem8  9017  kmlem13  9022  isfin1-3  9246  ac6num  9339  zorn2lem4  9359  fpwwe2lem12  9501  npomex  9856  genpnnp  9865  suplem2pr  9913  dedekind  10238  suprnub  11026  infregelb  11045  arch  11327  xrsupsslem  12175  xrinfmsslem  12176  supxrbnd1  12189  supxrbnd2  12190  supxrleub  12194  supxrbnd  12196  infxrgelb  12203  injresinjlem  12628  hashgt12el  13248  hashgt12el2  13249  sqrt2irr  15023  prmind2  15445  vdwnnlem3  15748  vdwnn  15749  acsfiindd  17224  isnmnd  17345  isnirred  18746  lssne0  18999  bwth  21261  t1connperf  21287  trfbas  21695  fbunfip  21720  fbasrn  21735  filuni  21736  hausflim  21832  alexsubALTlem3  21900  alexsubALTlem4  21901  ptcmplem4  21906  lebnumlem3  22809  bcthlem4  23170  bcth3  23174  amgm  24762  issqf  24907  ostth  25373  tglowdim2ln  25591  axcontlem12  25900  umgrnloop0  26049  numedglnl  26084  usgrnloop0ALT  26142  uhgrnbgr0nb  26295  nbgr0edg  26298  vtxd0nedgb  26440  vtxdusgr0edgnelALT  26448  1hevtxdg0  26457  usgrvd0nedg  26485  uhgrvd00  26486  pthdlem2lem  26719  nmounbi  27759  lnon0  27781  largei  29254  cvbr2  29270  chrelat2i  29352  uniinn0  29492  infxrge0gelb  29659  nn0min  29695  toslublem  29795  tosglblem  29797  archiabl  29880  lmdvg  30127  esumcvgre  30281  eulerpartlems  30550  bnj110  31054  bnj1417  31235  dfon2lem8  31819  nosupbnd1lem4  31982  sltrec  32049  dfint3  32184  unblimceq0  32623  relowlpssretop  33342  poimirlem26  33565  poimirlem30  33569  poimir  33572  mblfinlem1  33576  ftc1anc  33623  heiborlem1  33740  lcvbr2  34627  lcvbr3  34628  cvrnbtwn  34876  cvrval2  34879  hlrelat2  35007  cdleme0nex  35895  rencldnfilem  37701  setindtr  37908  gneispace  38749  nelrnmpt  39571  supxrgere  39862  supxrgelem  39866  infxrbnd2  39898  supminfxr  40007  limsupub  40254  limsuppnflem  40260  limsupre2lem  40274  stirlinglem5  40613  etransclem24  40793  etransclem32  40801  sge0iunmpt  40953  sge0rpcpnf  40956  iundjiun  40995  voliunsge0lem  41007  meaiuninc3v  41019  meaiininclem  41021  hoidmv1lelem3  41128  hoidmvlelem4  41133  hoidmvlelem5  41134  copisnmnd  42134  lindslinindsimp1  42571  lindslinindsimp2  42577  ldepslinc  42623  aacllem  42875
  Copyright terms: Public domain W3C validator