Theorem ralnex 3097

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

Step	Hyp	Ref	Expression
1		raln 3094	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
2		alnex 1808	. . 3 ⊢ (∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ¬ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3		df-rex 3096	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4	2, 3	xchbinxr 338	. 2 ⊢ (∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑)
5	1, 4	bitri 278	1 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 209   ∧ wa 400  ∀wal 1565  ∃wex 1806   ∈ wcel 2149  ∀wral 3085  ∃wrex 3095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-ral 3086  df-rex 3096

This theorem is referenced by:  dfrex2  3098  nrex  3099  rexim  3112  dfral2  3122  ralinexa  3124  r19.43  3139  ralnex2  3151  ralnex3  3152  nrexralim  3155  nrexdv  3166  nelb  3247  cbvrexdva  3252  cbvrexfw  3312  cbvrexdva2  3348  rexeqf  3353  rexprg  4668  n0snor2el  4802  iindif2  5047  rexiunxp  5827  rexxpf  5834  nelrnmpt  5958  f0rn0  6764  ordunisuc2  7840  tfi  7849  resf1extb  7931  releldmdifi  8042  omeulem1  8567  frfi  9245  isfinite2  9258  supmo  9412  infmo  9457  ordtypelem9  9488  elirrvOLDOLD  9561  unbndrank  9814  kmlem7  10140  kmlem8  10141  kmlem13  10146  isfin1-3  10370  ac6num  10463  zorn2lem4  10483  fpwwe2lem11  10626  npomex  10981  suplem2pr  11038  dedekind  11373  suprnub  12180  infregelb  12199  arch  12501  xrsupsslem  13333  xrinfmsslem  13334  supxrbnd1  13347  supxrbnd2  13348  supxrleub  13352  supxrbnd  13354  infxrgelb  13362  injresinjlem  13819  hashgt12el  14459  hashgt12el2  14460  sqrt2irr  16305  prmind2  16743  vdwnnlem3  17057  vdwnn  17058  acsfiindd  18609  isnmnd  18796  isnirred  20502  lssne0  21050  bwth  23536  t1connperf  23562  trfbas  23970  fbunfip  23995  fbasrn  24010  filuni  24011  hausflim  24107  alexsubALTlem3  24175  alexsubALTlem4  24176  ptcmplem4  24181  lebnumlem3  25091  bcthlem4  25455  bcth3  25459  amgm  27121  issqf  27266  ostth  27769  nosupbnd1lem4  27841  noinfbnd1lem4  27856  ltsrec  27960  cuteq1  27976  tglowdim2ln  28887  axcontlem12  29266  umgrnloop0  29400  numedglnl  29435  usgrnloop0ALT  29496  uhgrnbgr0nb  29645  nbgr0edg  29648  vtxd0nedgb  29779  vtxdusgr0edgnelALT  29787  1hevtxdg0  29796  usgrvd0nedg  29824  uhgrvd00  29825  pthdlem2lem  30057  nmounbi  31069  lnon0  31091  largei  32560  cvbr2  32576  chrelat2i  32658  n0nsnel  32802  uniinn0  32838  infxrge0gelb  33052  nn0min  33106  toslublem  33233  tosglblem  33235  archiabl  33459  lmdvg  34288  esumcvgre  34426  eulerpartlems  34695  bnj110  35191  bnj1417  35374  fineqvnttrclselem1  35467  lfuhgr3  35545  fmlaomn0  35815  fmla0disjsuc  35823  fmlasucdisj  35824  dfon2lem8  36213  dfint3  36377  bj-axseprep  37633  relowlpssretop  37932  domalom  37972  fvineqsneq  37980  poimirlem26  38219  poimirlem30  38223  poimir  38226  mblfinlem1  38230  ftc1anc  38274  heiborlem1  38384  lcvbr2  39720  lcvbr3  39721  cvrnbtwn  39969  cvrval2  39972  hlrelat2  40101  cdleme0nex  40988  aks4d1p7  42774  sticksstones1  42837  infdesc  43301  nna4b4nsq  43318  rencldnfilem  43473  setindtr  43677  onmaxnelsup  43876  onsupnmax  43881  onsupmaxb  43892  onsupeqnmax  43900  ordnexbtwnsuc  43920  gneispace  44786  iindif2f  45804  ralfal  45805  supxrgere  45975  supxrgelem  45979  infxrbnd2  46010  supminfxr  46104  limsupub  46344  limsuppnflem  46350  limsupre2lem  46364  stirlinglem5  46718  etransclem24  46898  etransclem32  46906  sge0iunmpt  47058  sge0rpcpnf  47061  iundjiun  47100  voliunsge0lem  47112  meaiuninc3v  47124  meaiininclem  47126  hoidmv1lelem3  47233  hoidmvlelem4  47238  hoidmvlelem5  47239  n0nsn2el  47685  0nelsetpreimafv  48062  nprmmul1  48199  stgr0  48648  gpg5nbgrvtx03starlem1  48756  gpg5nbgrvtx03starlem2  48757  gpg5nbgrvtx03starlem3  48758  gpg5nbgrvtx13starlem1  48759  gpg5nbgrvtx13starlem2  48760  gpg5nbgrvtx13starlem3  48761  gpg5edgnedg  48818  copisnmnd  48857  lindslinindsimp1  49156  lindslinindsimp2  49162  ldepslinc  49208  aacllem  50509