Theorem ralnex 3091

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

Syntax hints:  ¬ wn 3   ↔ wb 209   ∧ wa 400  ∀wal 1568  ∃wex 1809   ∈ wcel 2143  ∀wral 3079  ∃wrex 3089

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-ral 3080  df-rex 3090

This theorem is referenced by:  dfrex2  3092  nrex  3093  rexim  3106  dfral2  3116  ralinexa  3118  r19.43  3133  ralnex2  3145  ralnex3  3146  nrexralim  3149  nrexdv  3160  nelb  3241  cbvrexdva  3246  cbvrexfw  3306  cbvrexdva2  3341  rexeqf  3346  rexprg  4663  n0snor2el  4798  iindif2  5043  rexiunxp  5826  rexxpf  5833  nelrnmpt  5957  f0rn0  6763  ordunisuc2  7836  tfi  7845  resf1extb  7927  releldmdifi  8038  omeulem1  8563  frfi  9241  isfinite2  9254  supmo  9408  infmo  9453  ordtypelem9  9484  elirrvOLDOLD  9557  unbndrank  9810  kmlem7  10136  kmlem8  10137  kmlem13  10142  isfin1-3  10365  ac6num  10458  zorn2lem4  10478  fpwwe2lem11  10621  npomex  10976  suplem2pr  11033  dedekind  11368  suprnub  12175  infregelb  12194  arch  12496  xrsupsslem  13328  xrinfmsslem  13329  supxrbnd1  13342  supxrbnd2  13343  supxrleub  13347  supxrbnd  13349  infxrgelb  13357  injresinjlem  13815  hashgt12el  14455  hashgt12el2  14456  sqrt2irr  16300  prmind2  16738  vdwnnlem3  17052  vdwnn  17053  acsfiindd  18604  isnmnd  18791  isnirred  20498  lssne0  21072  bwth  23567  t1connperf  23593  trfbas  24001  fbunfip  24026  fbasrn  24041  filuni  24042  hausflim  24138  alexsubALTlem3  24206  alexsubALTlem4  24207  ptcmplem4  24212  lebnumlem3  25122  bcthlem4  25486  bcth3  25490  amgm  27155  issqf  27300  ostth  27803  nosupbnd1lem4  27875  noinfbnd1lem4  27890  ltsrec  27994  cuteq1  28010  tglowdim2ln  28925  axcontlem12  29325  umgrnloop0  29459  numedglnl  29494  usgrnloop0ALT  29555  uhgrnbgr0nb  29704  nbgr0edg  29707  vtxd0nedgb  29838  vtxdusgr0edgnelALT  29846  1hevtxdg0  29855  usgrvd0nedg  29883  uhgrvd00  29884  pthdlem2lem  30116  nmounbi  31128  lnon0  31150  largei  32619  cvbr2  32635  chrelat2i  32717  n0nsnel  32861  uniinn0  32897  infxrge0gelb  33111  nn0min  33165  toslublem  33292  tosglblem  33294  archiabl  33518  lmdvg  34343  esumcvgre  34481  eulerpartlems  34750  bnj110  35246  bnj1417  35429  fineqvnttrclselem1  35534  lfuhgr3  35612  fmlaomn0  35882  fmla0disjsuc  35890  fmlasucdisj  35891  dfon2lem8  36280  dfint3  36444  bj-axseprep  37731  relowlpssretop  38030  domalom  38070  fvineqsneq  38078  poimirlem26  38317  poimirlem30  38321  poimir  38324  mblfinlem1  38328  ftc1anc  38372  heiborlem1  38482  lcvbr2  39816  lcvbr3  39817  cvrnbtwn  40065  cvrval2  40068  hlrelat2  40197  cdleme0nex  41084  aks4d1p7  42870  sticksstones1  42933  infdesc  43395  nna4b4nsq  43412  rencldnfilem  43567  setindtr  43771  onmaxnelsup  43970  onsupnmax  43975  onsupmaxb  43986  onsupeqnmax  43994  ordnexbtwnsuc  44014  gneispace  44880  iindif2f  45898  ralfal  45899  supxrgere  46069  supxrgelem  46073  infxrbnd2  46104  supminfxr  46198  limsupub  46438  limsuppnflem  46444  limsupre2lem  46458  stirlinglem5  46812  etransclem24  46992  etransclem32  47000  sge0iunmpt  47152  sge0rpcpnf  47155  iundjiun  47194  voliunsge0lem  47206  meaiuninc3v  47218  meaiininclem  47220  hoidmv1lelem3  47327  hoidmvlelem4  47332  hoidmvlelem5  47333  n0nsn2el  47782  0nelsetpreimafv  48159  nprmmul1  48296  stgr0  48745  gpg5nbgrvtx03starlem1  48853  gpg5nbgrvtx03starlem2  48854  gpg5nbgrvtx03starlem3  48855  gpg5nbgrvtx13starlem1  48856  gpg5nbgrvtx13starlem2  48857  gpg5nbgrvtx13starlem3  48858  gpg5edgnedg  48915  copisnmnd  48954  lindslinindsimp1  49257  lindslinindsimp2  49263  ldepslinc  49309  aacllem  50641