Theorem ralnex 3055

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 3052	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
2		alnex 1781	. . 3 ⊢ (∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ¬ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3		df-rex 3054	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4	2, 3	xchbinxr 335	. 2 ⊢ (∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑)
5	1, 4	bitri 275	1 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395  ∀wal 1538  ∃wex 1779   ∈ wcel 2109  ∀wral 3044  ∃wrex 3053

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-ral 3045  df-rex 3054

This theorem is referenced by:  dfrex2  3056  nrex  3057  rexim  3070  dfral2  3080  ralinexa  3082  r19.43  3097  ralnex2  3109  ralnex3  3110  nrexralim  3113  nrexdv  3124  nelb  3205  cbvrexdva  3210  cbvrexfw  3270  rexeqbidvvOLD  3300  cbvrexdva2  3312  rexeqf  3319  rexprg  4647  n0snor2el  4782  iindif2  5022  rexiunxp  5777  rexxpf  5784  f0rn0  6703  ordunisuc2  7768  tfi  7777  resf1extb  7858  releldmdifi  7971  omeulem1  8491  frfi  9163  isfinite2  9176  supmo  9330  infmo  9375  ordtypelem9  9406  elirrvOLD  9478  unbndrank  9726  kmlem7  10039  kmlem8  10040  kmlem13  10045  isfin1-3  10268  ac6num  10361  zorn2lem4  10381  fpwwe2lem11  10523  npomex  10878  suplem2pr  10935  dedekind  11267  suprnub  12078  infregelb  12097  arch  12369  xrsupsslem  13197  xrinfmsslem  13198  supxrbnd1  13211  supxrbnd2  13212  supxrleub  13216  supxrbnd  13218  infxrgelb  13226  injresinjlem  13678  hashgt12el  14317  hashgt12el2  14318  sqrt2irr  16145  prmind2  16583  vdwnnlem3  16896  vdwnn  16897  acsfiindd  18446  isnmnd  18599  isnirred  20292  lssne0  20838  bwth  23279  t1connperf  23305  trfbas  23713  fbunfip  23738  fbasrn  23753  filuni  23754  hausflim  23850  alexsubALTlem3  23918  alexsubALTlem4  23919  ptcmplem4  23924  lebnumlem3  24843  bcthlem4  25208  bcth3  25212  amgm  26882  issqf  27027  ostth  27531  nosupbnd1lem4  27604  noinfbnd1lem4  27619  sltrec  27716  cuteq1  27732  tglowdim2ln  28583  axcontlem12  28907  umgrnloop0  29041  numedglnl  29076  usgrnloop0ALT  29137  uhgrnbgr0nb  29286  nbgr0edg  29289  vtxd0nedgb  29421  vtxdusgr0edgnelALT  29429  1hevtxdg0  29438  usgrvd0nedg  29466  uhgrvd00  29467  pthdlem2lem  29699  nmounbi  30707  lnon0  30729  largei  32198  cvbr2  32214  chrelat2i  32296  n0nsnel  32447  uniinn0  32482  infxrge0gelb  32701  nn0min  32758  toslublem  32909  tosglblem  32911  archiabl  33135  lmdvg  33934  esumcvgre  34072  eulerpartlems  34341  bnj110  34838  bnj1417  35021  fineqvnttrclselem1  35087  lfuhgr3  35110  fmlaomn0  35380  fmla0disjsuc  35388  fmlasucdisj  35389  dfon2lem8  35781  dfint3  35943  relowlpssretop  37355  domalom  37395  fvineqsneq  37403  poimirlem26  37643  poimirlem30  37647  poimir  37650  mblfinlem1  37654  ftc1anc  37698  heiborlem1  37808  lcvbr2  39018  lcvbr3  39019  cvrnbtwn  39267  cvrval2  39270  hlrelat2  39399  cdleme0nex  40286  aks4d1p7  42073  sticksstones1  42136  infdesc  42633  nna4b4nsq  42650  rencldnfilem  42810  setindtr  43014  onmaxnelsup  43213  onsupnmax  43218  onsupmaxb  43229  onsupeqnmax  43237  ordnexbtwnsuc  43257  gneispace  44124  nelrnmpt  45078  iindif2f  45154  ralfal  45155  supxrgere  45329  supxrgelem  45333  infxrbnd2  45364  supminfxr  45459  limsupub  45699  limsuppnflem  45705  limsupre2lem  45719  stirlinglem5  46073  etransclem24  46253  etransclem32  46261  sge0iunmpt  46413  sge0rpcpnf  46416  iundjiun  46455  voliunsge0lem  46467  meaiuninc3v  46479  meaiininclem  46481  hoidmv1lelem3  46588  hoidmvlelem4  46593  hoidmvlelem5  46594  n0nsn2el  47023  0nelsetpreimafv  47388  stgr0  47958  gpg5nbgrvtx03starlem1  48066  gpg5nbgrvtx03starlem2  48067  gpg5nbgrvtx03starlem3  48068  gpg5nbgrvtx13starlem1  48069  gpg5nbgrvtx13starlem2  48070  gpg5nbgrvtx13starlem3  48071  gpg5edgnedg  48128  copisnmnd  48167  lindslinindsimp1  48456  lindslinindsimp2  48462  ldepslinc  48508  aacllem  49800