Theorem ralnex 3089

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

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   ∧ wa 401  ∀wal 1568  ∃wex 1812   ∈ wcel 2145  ∀wral 3077  ∃wrex 3087

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-ral 3078  df-rex 3088

This theorem is used by:  dfrex2  3090  nrex  3091  rexim  3104  dfral2  3114  ralinexa  3116  r19.43  3131  ralnex2  3143  ralnex3  3144  nrexralim  3147  nrexdv  3158  nelb  3239  cbvrexdva  3244  cbvrexfw  3304  cbvrexdva2  3338  rexeqf  3343  rexprg  4658  n0snor2el  4793  iindif2  5037  rexiunxp  5817  rexxpf  5825  nelrnmpt  5949  f0rn0  6767  ordunisuc2  7855  tfi  7864  resf1extb  7946  releldmdifi  8056  omeulem1  8590  frfi  9276  isfinite2  9290  supmo  9444  infmo  9489  ordtypelem9  9520  elirrvOLDOLD  9593  unbndrank  9855  kmlem7  10235  kmlem8  10236  kmlem13  10241  isfin1-3  10464  ac6num  10557  zorn2lem4  10577  fpwwe2lem11  10726  npomex  11081  suplem2pr  11138  dedekind  11473  suprnub  12282  infregelb  12301  arch  12603  xrsupsslem  13437  xrinfmsslem  13438  supxrbnd1  13451  supxrbnd2  13452  supxrleub  13456  supxrbnd  13458  infxrgelb  13466  injresinjlem  13925  hashgt12el  14567  hashgt12el2  14568  sqrt2irr  16417  prmind2  16860  vdwnnlem3  17175  vdwnn  17176  acsfiindd  18727  isnmnd  18927  isnirred  20650  lssne0  21226  bwth  23728  t1connperf  23754  trfbas  24163  fbunfip  24188  fbasrn  24203  filuni  24204  hausflim  24300  alexsubALTlem3  24368  alexsubALTlem4  24369  ptcmplem4  24374  lebnumlem3  25284  bcthlem4  25648  bcth3  25652  amgm  27318  issqf  27463  ostth  27966  infdesc  27967  nna4b4nsq  27990  nosupbnd1lem4  28068  noinfbnd1lem4  28083  ltsrec  28187  cuteq1  28203  tglowdim2ln  29120  axcontlem12  29553  umgrnloop0  29687  numedglnl  29722  lfuhgr3  29728  usgrnloop0ALT  29786  uhgrnbgr0nb  29935  nbgr0edg  29938  vtxd0nedgb  30069  vtxdusgr0edgnelALT  30077  1hevtxdg0  30086  usgrvd0nedg  30114  uhgrvd00  30115  pthdlem2lem  30353  nmounbi  31378  lnon0  31400  largei  32869  cvbr2  32885  chrelat2i  32967  n0nsnel  33111  uniinn0  33147  infxrge0gelb  33358  nn0min  33412  toslublem  33533  tosglblem  33535  archiabl  33759  lmdvg  34585  esumcvgre  34723  eulerpartlems  34992  bnj110  35488  bnj1417  35671  fineqvnttrclselem1  35789  fmlaomn0  36155  fmla0disjsuc  36163  fmlasucdisj  36164  dfon2lem8  36552  dfint3  36716  dffr7  36720  bj-axseprep  37990  relowlpssretop  38287  domalom  38327  fvineqsneq  38335  poimirlem26  38564  poimirlem30  38568  poimir  38571  mblfinlem1  38575  ftc1anc  38619  heiborlem1  38745  lcvbr2  40079  lcvbr3  40080  cvrnbtwn  40328  cvrval2  40331  hlrelat2  40460  cdleme0nex  41347  aks4d1p7  43133  sticksstones1  43196  rencldnfilem  43826  setindtr  44030  onmaxnelsup  44224  onsupnmax  44229  onsupmaxb  44240  onsupeqnmax  44248  ordnexbtwnsuc  44268  gneispace  45133  iindif2f  46174  ralfal  46175  supxrgere  46344  supxrgelem  46348  infxrbnd2  46379  supminfxr  46473  limsupub  46713  limsuppnflem  46719  limsupre2lem  46733  stirlinglem5  47087  etransclem24  47267  etransclem32  47275  sge0iunmpt  47427  sge0rpcpnf  47430  iundjiun  47469  voliunsge0lem  47481  meaiuninc3v  47493  meaiininclem  47495  hoidmv1lelem3  47602  hoidmvlelem4  47607  hoidmvlelem5  47608  n0nsn2el  48094  0nelsetpreimafv  48471  nprmmul1  48608  stgr0  49057  gpg5nbgrvtx03starlem1  49165  gpg5nbgrvtx03starlem2  49166  gpg5nbgrvtx03starlem3  49167  gpg5nbgrvtx13starlem1  49168  gpg5nbgrvtx13starlem2  49169  gpg5nbgrvtx13starlem3  49170  gpg5edgnedg  49227  copisnmnd  49265  lindslinindsimp1  49568  lindslinindsimp2  49574  ldepslinc  49620  aacllem  50938