Theorem ralnex 3199

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 3123	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
2		alnex 1783	. . 3 ⊢ (∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ¬ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3		df-rex 3112	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4	2, 3	xchbinxr 338	. 2 ⊢ (∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑)
5	1, 4	bitri 278	1 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 209   ∧ wa 399  ∀wal 1536  ∃wex 1781   ∈ wcel 2111  ∀wral 3106  ∃wrex 3107

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 3111  df-rex 3112

This theorem is referenced by:  dfral2  3200  dfrex2  3202  ralnex2  3221  ralnex3  3222  ralinexa  3223  nrexralim  3225  nelb  3227  nrex  3228  nrexdv  3229  r19.30  3293  r19.43  3304  n0snor2el  4724  iindif2  4962  rexiunxp  5675  rexxpf  5682  f0rn0  6538  ordunisuc2  7539  tfi  7548  releldmdifi  7726  omeulem1  8191  frfi  8747  isfinite2  8760  supmo  8900  infmo  8943  ordtypelem9  8974  elirrv  9044  unbndrank  9255  kmlem7  9567  kmlem8  9568  kmlem13  9573  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  15594  prmind2  16019  vdwnnlem3  16323  vdwnn  16324  acsfiindd  17779  isnmnd  17907  isnirred  19446  lssne0  19715  bwth  22015  t1connperf  22041  trfbas  22449  fbunfip  22474  fbasrn  22489  filuni  22490  hausflim  22586  alexsubALTlem3  22654  alexsubALTlem4  22655  ptcmplem4  22660  lebnumlem3  23568  bcthlem4  23931  bcth3  23935  amgm  25576  issqf  25721  ostth  26223  tglowdim2ln  26445  axcontlem12  26769  umgrnloop0  26902  numedglnl  26937  usgrnloop0ALT  26995  uhgrnbgr0nb  27144  nbgr0edg  27147  vtxd0nedgb  27278  vtxdusgr0edgnelALT  27286  1hevtxdg0  27295  usgrvd0nedg  27323  uhgrvd00  27324  pthdlem2lem  27556  nmounbi  28559  lnon0  28581  largei  30050  cvbr2  30066  chrelat2i  30148  uniinn0  30314  infxrge0gelb  30516  nn0min  30562  toslublem  30680  tosglblem  30682  archiabl  30877  lmdvg  31306  esumcvgre  31460  eulerpartlems  31728  bnj110  32240  bnj1417  32423  lfuhgr3  32479  fmlaomn0  32750  fmla0disjsuc  32758  fmlasucdisj  32759  dfon2lem8  33148  nosupbnd1lem4  33324  sltrec  33391  dfint3  33526  relowlpssretop  34781  domalom  34821  fvineqsneq  34829  poimirlem26  35083  poimirlem30  35087  poimir  35090  mblfinlem1  35094  ftc1anc  35138  heiborlem1  35249  lcvbr2  36318  lcvbr3  36319  cvrnbtwn  36567  cvrval2  36570  hlrelat2  36699  cdleme0nex  37586  rencldnfilem  39761  setindtr  39965  gneispace  40837  nelrnmpt  41720  supxrgere  41965  supxrgelem  41969  infxrbnd2  42001  supminfxr  42103  limsupub  42346  limsuppnflem  42352  limsupre2lem  42366  stirlinglem5  42720  etransclem24  42900  etransclem32  42908  sge0iunmpt  43057  sge0rpcpnf  43060  iundjiun  43099  voliunsge0lem  43111  meaiuninc3v  43123  meaiininclem  43125  hoidmv1lelem3  43232  hoidmvlelem4  43237  hoidmvlelem5  43238  0nelsetpreimafv  43907  copisnmnd  44429  lindslinindsimp1  44866  lindslinindsimp2  44872  ldepslinc  44918  aacllem  45329