Theorem ralnex 3088

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 3085	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
2		alnex 1814	. . 3 ⊢ (∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ¬ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3		df-rex 3087	. . 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 3076  ∃wrex 3086

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 3077  df-rex 3087

This theorem is used by:  dfrex2  3089  nrex  3090  rexim  3103  dfral2  3113  ralinexa  3115  r19.43  3130  ralnex2  3142  ralnex3  3143  nrexralim  3146  nrexdv  3157  nelb  3238  cbvrexdva  3243  cbvrexfw  3303  cbvrexdva2  3337  rexeqf  3342  rexprg  4658  n0snor2el  4793  iindif2  5037  rexiunxp  5820  rexxpf  5827  nelrnmpt  5951  f0rn0  6761  ordunisuc2  7841  tfi  7850  resf1extb  7932  releldmdifi  8043  omeulem1  8572  frfi  9258  isfinite2  9271  supmo  9425  infmo  9470  ordtypelem9  9501  elirrvOLDOLD  9574  unbndrank  9827  kmlem7  10162  kmlem8  10163  kmlem13  10168  isfin1-3  10391  ac6num  10484  zorn2lem4  10504  fpwwe2lem11  10653  npomex  11008  suplem2pr  11065  dedekind  11400  suprnub  12207  infregelb  12226  arch  12528  xrsupsslem  13362  xrinfmsslem  13363  supxrbnd1  13376  supxrbnd2  13377  supxrleub  13381  supxrbnd  13383  infxrgelb  13391  injresinjlem  13849  hashgt12el  14490  hashgt12el2  14491  sqrt2irr  16340  prmind2  16778  vdwnnlem3  17092  vdwnn  17093  acsfiindd  18644  isnmnd  18843  isnirred  20564  lssne0  21138  bwth  23638  t1connperf  23664  trfbas  24073  fbunfip  24098  fbasrn  24113  filuni  24114  hausflim  24210  alexsubALTlem3  24278  alexsubALTlem4  24279  ptcmplem4  24284  lebnumlem3  25194  bcthlem4  25558  bcth3  25562  amgm  27230  issqf  27375  ostth  27878  nosupbnd1lem4  27950  noinfbnd1lem4  27965  ltsrec  28069  cuteq1  28085  tglowdim2ln  29002  axcontlem12  29435  umgrnloop0  29569  numedglnl  29604  lfuhgr3  29610  usgrnloop0ALT  29668  uhgrnbgr0nb  29817  nbgr0edg  29820  vtxd0nedgb  29951  vtxdusgr0edgnelALT  29959  1hevtxdg0  29968  usgrvd0nedg  29996  uhgrvd00  29997  pthdlem2lem  30235  nmounbi  31260  lnon0  31282  largei  32751  cvbr2  32767  chrelat2i  32849  n0nsnel  32993  uniinn0  33029  infxrge0gelb  33240  nn0min  33294  toslublem  33415  tosglblem  33417  archiabl  33641  lmdvg  34466  esumcvgre  34604  eulerpartlems  34874  bnj110  35370  bnj1417  35553  fineqvnttrclselem1  35650  fmlaomn0  35972  fmla0disjsuc  35980  fmlasucdisj  35981  dfon2lem8  36370  dfint3  36534  dffr7  36538  bj-axseprep  37822  relowlpssretop  38121  domalom  38161  fvineqsneq  38169  poimirlem26  38398  poimirlem30  38402  poimir  38405  mblfinlem1  38409  ftc1anc  38453  heiborlem1  38564  lcvbr2  39898  lcvbr3  39899  cvrnbtwn  40147  cvrval2  40150  hlrelat2  40279  cdleme0nex  41166  aks4d1p7  42952  sticksstones1  43015  infdesc  43492  nna4b4nsq  43509  rencldnfilem  43664  setindtr  43868  onmaxnelsup  44067  onsupnmax  44072  onsupmaxb  44083  onsupeqnmax  44091  ordnexbtwnsuc  44111  gneispace  44977  iindif2f  45995  ralfal  45996  supxrgere  46166  supxrgelem  46170  infxrbnd2  46201  supminfxr  46295  limsupub  46535  limsuppnflem  46541  limsupre2lem  46555  stirlinglem5  46909  etransclem24  47089  etransclem32  47097  sge0iunmpt  47249  sge0rpcpnf  47252  iundjiun  47291  voliunsge0lem  47303  meaiuninc3v  47315  meaiininclem  47317  hoidmv1lelem3  47424  hoidmvlelem4  47429  hoidmvlelem5  47430  n0nsn2el  47916  0nelsetpreimafv  48293  nprmmul1  48430  stgr0  48879  gpg5nbgrvtx03starlem1  48987  gpg5nbgrvtx03starlem2  48988  gpg5nbgrvtx03starlem3  48989  gpg5nbgrvtx13starlem1  48990  gpg5nbgrvtx13starlem2  48991  gpg5nbgrvtx13starlem3  48992  gpg5edgnedg  49049  copisnmnd  49087  lindslinindsimp1  49390  lindslinindsimp2  49396  ldepslinc  49442  aacllem  50775