Theorem ralnex 2975

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 2974	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
2		alnex 1697	. . 3 ⊢ (∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ¬ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3		df-rex 2902	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4	2, 3	xchbinxr 324	. 2 ⊢ (∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑)
5	1, 4	bitri 263	1 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 195   ∧ wa 383  ∀wal 1473  ∃wex 1695   ∈ wcel 1977  ∀wral 2896  ∃wrex 2897

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

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-ral 2901  df-rex 2902

This theorem is referenced by:  dfral2  2977  dfrex2  2979  ralinexa  2980  nrexralim  2982  nrex  2983  nrexdv  2984  r19.43  3074  rabeq0OLD  3914  n0snor2el  4304  iindif2  4525  rexiunxp  5184  rexxpf  5191  f0rn0  6003  ordunisuc2  6936  tfi  6945  omeulem1  7549  frfi  8090  isfinite2  8103  supmo  8241  infmo  8284  ordtypelem9  8314  elirrv  8387  unbndrank  8588  kmlem7  8861  kmlem8  8862  kmlem13  8867  isfin1-3  9091  ac6num  9184  zorn2lem4  9204  fpwwe2lem12  9342  npomex  9697  genpnnp  9706  suplem2pr  9754  dedekind  10079  suprnub  10865  infregelb  10884  arch  11166  xrsupsslem  12009  xrinfmsslem  12010  supxrbnd1  12023  supxrbnd2  12024  supxrleub  12028  supxrbnd  12030  infxrgelb  12037  injresinjlem  12450  hashgt12el  13070  hashgt12el2  13071  sqrt2irr  14817  prmind2  15236  vdwnnlem3  15539  vdwnn  15540  acsfiindd  17000  isnmnd  17121  isnirred  18523  lssne0  18772  bwth  21023  t1conperf  21049  trfbas  21458  fbunfip  21483  fbasrn  21498  filuni  21499  hausflim  21595  alexsubALTlem3  21663  alexsubALTlem4  21664  ptcmplem4  21669  lebnumlem3  22570  bcthlem4  22932  bcth3  22936  amgm  24517  issqf  24662  ostth  25128  tglowdim2ln  25346  axcontlem12  25655  umgrnloop0  25775  usgranloop0  25909  vdusgra0nedg  26435  usgravd0nedg  26445  usgravd00  26446  nmounbi  27015  lnon0  27037  largei  28510  cvbr2  28526  chrelat2i  28608  uniinn0  28749  infxrge0gelb  28921  nn0min  28954  toslublem  28998  tosglblem  29000  archiabl  29083  lmdvg  29327  esumcvgre  29480  eulerpartlems  29749  bnj110  30182  bnj1417  30363  dfon2lem8  30939  dfint3  31229  unblimceq0  31668  relowlpssretop  32388  poimirlem26  32605  poimirlem30  32609  poimir  32612  mblfinlem1  32616  ftc1anc  32663  heiborlem1  32780  lcvbr2  33327  lcvbr3  33328  cvrnbtwn  33576  cvrval2  33579  hlrelat2  33707  cdleme0nex  34595  rencldnfilem  36402  setindtr  36609  gneispace  37452  nelrnmpt  38283  supxrgere  38490  supxrgelem  38494  infxrbnd2  38526  stirlinglem5  38971  etransclem24  39151  etransclem32  39159  sge0iunmpt  39311  sge0rpcpnf  39314  iundjiun  39353  voliunsge0lem  39365  meaiininclem  39376  hoidmv1lelem3  39483  hoidmvlelem4  39488  hoidmvlelem5  39489  usgrnloop0ALT  40432  uhgrnbgr0nb  40576  nbgr0edg  40579  vtxd0nedgb  40703  vtxdusgr0edgnelALT  40711  1hevtxdg0  40720  usgrvd0nedg  40749  uhgrvd00  40750  pthdlem2lem  40973  copisnmnd  41599  lindslinindsimp1  42040  lindslinindsimp2  42046  ldepslinc  42092  aacllem  42356