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 1813	. . 3 ⊢ (∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ¬ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3		df-rex 3090	. . 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 1567  ∃wex 1811   ∈ wcel 2146  ∀wral 3079  ∃wrex 3089

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

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-ral 3080  df-rex 3090

This theorem is used 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  3340  rexeqf  3345  rexprg  4657  n0snor2el  4790  iindif2  5039  rexiunxp  5821  rexxpf  5829  nelrnmpt  5953  f0rn0  6775  ordunisuc2  7862  tfi  7871  resf1extb  7953  releldmdifi  8064  omeulem1  8601  frfi  9287  isfinite2  9301  supmo  9454  infmo  9499  ordtypelem9  9530  elirrvOLDOLD  9603  unbndrank  9865  kmlem7  10245  kmlem8  10246  kmlem13  10251  isfin1-3  10474  ac6num  10567  zorn2lem4  10587  fpwwe2lem11  10736  npomex  11091  suplem2pr  11148  dedekind  11483  suprnub  12292  infregelb  12311  arch  12613  xrsupsslem  13447  xrinfmsslem  13448  supxrbnd1  13461  supxrbnd2  13462  supxrleub  13466  supxrbnd  13468  infxrgelb  13476  injresinjlem  13935  hashgt12el  14577  hashgt12el2  14578  sqrt2irr  16429  prmind2  16872  vdwnnlem3  17187  vdwnn  17188  acsfiindd  18739  isnmnd  18939  isnirred  20662  lssne0  21238  bwth  23740  t1connperf  23766  trfbas  24175  fbunfip  24200  fbasrn  24215  filuni  24216  hausflim  24312  alexsubALTlem3  24380  alexsubALTlem4  24381  ptcmplem4  24386  lebnumlem3  25296  bcthlem4  25660  bcth3  25664  amgm  27330  issqf  27475  ostth  27978  infdesc  27979  nna4b4nsq  28002  nosupbnd1lem4  28080  noinfbnd1lem4  28095  ltsrec  28199  cuteq1  28215  tglowdim2ln  29132  axcontlem12  29565  umgrnloop0  29699  numedglnl  29734  lfuhgr3  29740  usgrnloop0ALT  29798  uhgrnbgr0nb  29947  nbgr0edg  29950  vtxd0nedgb  30081  vtxdusgr0edgnelALT  30089  1hevtxdg0  30098  usgrvd0nedg  30126  uhgrvd00  30127  pthdlem2lem  30365  nmounbi  31390  lnon0  31412  largei  32881  cvbr2  32897  chrelat2i  32979  n0nsnel  33165  uniinn0  33201  infxrge0gelb  33411  nn0min  33465  toslublem  33586  tosglblem  33588  archiabl  33812  lmdvg  34638  esumcvgre  34776  eulerpartlems  35045  bnj110  35541  bnj1417  35724  fineqvnttrclselem1  35860  fmlaomn0  36276  fmla0disjsuc  36284  fmlasucdisj  36285  dfon2lem8  36679  dfint3  36843  dffr7  36847  bj-axseprep  38129  relowlpssretop  38427  domalom  38467  fvineqsneq  38475  poimirlem26  38704  poimirlem30  38708  poimir  38711  mblfinlem1  38715  ftc1anc  38759  heiborlem1  38885  lcvbr2  40219  lcvbr3  40220  cvrnbtwn  40468  cvrval2  40471  hlrelat2  40600  cdleme0nex  41487  aks4d1p7  43273  sticksstones1  43336  rencldnfilem  43967  setindtr  44171  onmaxnelsup  44365  onsupnmax  44370  onsupmaxb  44381  onsupeqnmax  44389  ordnexbtwnsuc  44409  gneispace  45274  iindif2f  46314  ralfal  46315  supxrgere  46484  supxrgelem  46488  infxrbnd2  46519  supminfxr  46613  limsupub  46853  limsuppnflem  46859  limsupre2lem  46873  stirlinglem5  47227  etransclem24  47407  etransclem32  47415  sge0iunmpt  47567  sge0rpcpnf  47570  iundjiun  47609  voliunsge0lem  47621  meaiuninc3v  47633  meaiininclem  47635  hoidmv1lelem3  47742  hoidmvlelem4  47747  hoidmvlelem5  47748  n0nsn2el  48234  0nelsetpreimafv  48611  nprmmul1  48748  stgr0  49197  gpg5nbgrvtx03starlem1  49305  gpg5nbgrvtx03starlem2  49306  gpg5nbgrvtx03starlem3  49307  gpg5nbgrvtx13starlem1  49308  gpg5nbgrvtx13starlem2  49309  gpg5nbgrvtx13starlem3  49310  gpg5edgnedg  49367  copisnmnd  49405  lindslinindsimp1  49708  lindslinindsimp2  49714  ldepslinc  49760  aacllem  51153