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

Theorem ralnex 2970
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 2969 . 2 (∀𝑥𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥𝐴𝜑))
2 alnex 1696 . . 3 (∀𝑥 ¬ (𝑥𝐴𝜑) ↔ ¬ ∃𝑥(𝑥𝐴𝜑))
3 df-rex 2897 . . 3 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
42, 3xchbinxr 323 . 2 (∀𝑥 ¬ (𝑥𝐴𝜑) ↔ ¬ ∃𝑥𝐴 𝜑)
51, 4bitri 262 1 (∀𝑥𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 194  wa 382  wal 1472  wex 1694  wcel 1975  wral 2891  wrex 2892
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-ral 2896  df-rex 2897
This theorem is referenced by:  dfral2  2972  dfrex2  2974  ralinexa  2975  nrexralim  2977  nrex  2978  nrexdv  2979  r19.43  3069  rabeq0OLD  3909  iindif2  4515  rexiunxp  5168  rexxpf  5175  f0rn0  5984  ordunisuc2  6909  tfi  6918  omeulem1  7522  frfi  8063  isfinite2  8076  supmo  8214  infmo  8257  ordtypelem9  8287  elirrv  8360  unbndrank  8561  kmlem7  8834  kmlem8  8835  kmlem13  8840  isfin1-3  9064  ac6num  9157  zorn2lem4  9177  fpwwe2lem12  9315  npomex  9670  genpnnp  9679  suplem2pr  9727  dedekind  10047  suprnub  10831  infregelb  10850  arch  11132  xrsupsslem  11961  xrinfmsslem  11962  supxrbnd1  11975  supxrbnd2  11976  supxrleub  11980  supxrbnd  11982  infxrgelb  11989  injresinjlem  12401  hashgt12el  13018  hashgt12el2  13019  sqrt2irr  14759  prmind2  15178  vdwnnlem3  15481  vdwnn  15482  acsfiindd  16942  isnmnd  17063  isnirred  18465  lssne0  18714  bwth  20961  t1conperf  20987  trfbas  21396  fbunfip  21421  fbasrn  21436  filuni  21437  hausflim  21533  alexsubALTlem3  21601  alexsubALTlem4  21602  ptcmplem4  21607  lebnumlem3  22497  bcthlem4  22845  bcth3  22849  amgm  24430  issqf  24575  ostth  25041  tglowdim2ln  25260  axcontlem12  25569  usgranloop0  25671  vdusgra0nedg  26197  usgravd0nedg  26207  usgravd00  26208  nmounbi  26817  lnon0  26839  largei  28312  cvbr2  28328  chrelat2i  28410  uniinn0  28551  infxrge0gelb  28723  nn0min  28756  toslublem  28800  tosglblem  28802  archiabl  28885  lmdvg  29129  esumcvgre  29282  eulerpartlems  29551  bnj110  29984  bnj1417  30165  dfon2lem8  30741  dfint3  31031  unblimceq0  31470  relowlpssretop  32187  poimirlem26  32404  poimirlem30  32408  poimir  32411  mblfinlem1  32415  ftc1anc  32462  heiborlem1  32579  lcvbr2  33126  lcvbr3  33127  cvrnbtwn  33375  cvrval2  33378  hlrelat2  33506  cdleme0nex  34394  rencldnfilem  36201  setindtr  36408  gneispace  37251  nelrnmpt  38082  supxrgere  38290  supxrgelem  38294  infxrbnd2  38326  stirlinglem5  38771  etransclem24  38951  etransclem32  38959  sge0iunmpt  39111  sge0rpcpnf  39114  iundjiun  39153  voliunsge0lem  39165  meaiininclem  39176  hoidmv1lelem3  39283  hoidmvlelem4  39288  hoidmvlelem5  39289  n0snor2el  40119  umgrnloop0  40332  usgrnloop0ALT  40430  uhgrnbgr0nb  40574  nbgr0edg  40577  vtxd0nedgb  40701  vtxdusgr0edgnelALT  40709  1hevtxdg0  40718  usgrvd0nedg  40747  uhgrvd00  40748  pthdlem2lem  40971  copisnmnd  41597  lindslinindsimp1  42038  lindslinindsimp2  42044  ldepslinc  42090  aacllem  42315
  Copyright terms: Public domain W3C validator