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

Theorem ralnex 3224
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 3147 . 2 (∀𝑥𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥𝐴𝜑))
2 alnex 1783 . . 3 (∀𝑥 ¬ (𝑥𝐴𝜑) ↔ ¬ ∃𝑥(𝑥𝐴𝜑))
3 df-rex 3136 . . 3 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
42, 3xchbinxr 338 . 2 (∀𝑥 ¬ (𝑥𝐴𝜑) ↔ ¬ ∃𝑥𝐴 𝜑)
51, 4bitri 278 1 (∀𝑥𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 209  wa 399  wal 1536  wex 1781  wcel 2114  wral 3130  wrex 3131
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-ral 3135  df-rex 3136
This theorem is referenced by:  dfral2  3225  dfrex2  3227  ralnex2  3248  ralnex3  3249  ralinexa  3250  nrexralim  3252  nelb  3254  nrex  3255  nrexdv  3256  r19.30  3321  r19.43  3332  n0snor2el  4737  iindif2  4974  rexiunxp  5688  rexxpf  5695  f0rn0  6545  ordunisuc2  7544  tfi  7553  releldmdifi  7730  omeulem1  8195  frfi  8751  isfinite2  8764  supmo  8904  infmo  8947  ordtypelem9  8978  elirrv  9048  unbndrank  9259  kmlem7  9571  kmlem8  9572  kmlem13  9577  isfin1-3  9797  ac6num  9890  zorn2lem4  9910  fpwwe2lem12  10052  npomex  10407  suplem2pr  10464  dedekind  10792  suprnub  11593  infregelb  11612  arch  11882  xrsupsslem  12688  xrinfmsslem  12689  supxrbnd1  12702  supxrbnd2  12703  supxrleub  12707  supxrbnd  12709  infxrgelb  12716  injresinjlem  13152  hashgt12el  13779  hashgt12el2  13780  sqrt2irr  15593  prmind2  16018  vdwnnlem3  16322  vdwnn  16323  acsfiindd  17778  isnmnd  17906  isnirred  19444  lssne0  19713  bwth  22013  t1connperf  22039  trfbas  22447  fbunfip  22472  fbasrn  22487  filuni  22488  hausflim  22584  alexsubALTlem3  22652  alexsubALTlem4  22653  ptcmplem4  22658  lebnumlem3  23566  bcthlem4  23929  bcth3  23933  amgm  25574  issqf  25719  ostth  26221  tglowdim2ln  26443  axcontlem12  26767  umgrnloop0  26900  numedglnl  26935  usgrnloop0ALT  26993  uhgrnbgr0nb  27142  nbgr0edg  27145  vtxd0nedgb  27276  vtxdusgr0edgnelALT  27284  1hevtxdg0  27293  usgrvd0nedg  27321  uhgrvd00  27322  pthdlem2lem  27554  nmounbi  28557  lnon0  28579  largei  30048  cvbr2  30064  chrelat2i  30146  uniinn0  30309  infxrge0gelb  30500  nn0min  30546  toslublem  30664  tosglblem  30666  archiabl  30858  lmdvg  31270  esumcvgre  31424  eulerpartlems  31692  bnj110  32204  bnj1417  32387  lfuhgr3  32440  fmlaomn0  32711  fmla0disjsuc  32719  fmlasucdisj  32720  dfon2lem8  33109  nosupbnd1lem4  33285  sltrec  33352  dfint3  33487  relowlpssretop  34742  domalom  34782  fvineqsneq  34790  poimirlem26  35041  poimirlem30  35045  poimir  35048  mblfinlem1  35052  ftc1anc  35096  heiborlem1  35207  lcvbr2  36276  lcvbr3  36277  cvrnbtwn  36525  cvrval2  36528  hlrelat2  36657  cdleme0nex  37544  rencldnfilem  39691  setindtr  39895  gneispace  40770  nelrnmpt  41654  supxrgere  41904  supxrgelem  41908  infxrbnd2  41940  supminfxr  42042  limsupub  42285  limsuppnflem  42291  limsupre2lem  42305  stirlinglem5  42659  etransclem24  42839  etransclem32  42847  sge0iunmpt  42996  sge0rpcpnf  42999  iundjiun  43038  voliunsge0lem  43050  meaiuninc3v  43062  meaiininclem  43064  hoidmv1lelem3  43171  hoidmvlelem4  43176  hoidmvlelem5  43177  0nelsetpreimafv  43846  copisnmnd  44368  lindslinindsimp1  44805  lindslinindsimp2  44811  ldepslinc  44857  aacllem  45268
  Copyright terms: Public domain W3C validator