Theorem ralnex 3058

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395  ∀wal 1539  ∃wex 1780   ∈ wcel 2111  ∀wral 3047  ∃wrex 3056

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-ral 3048  df-rex 3057

This theorem is referenced by:  dfrex2  3059  nrex  3060  rexim  3073  dfral2  3083  ralinexa  3085  r19.43  3100  ralnex2  3112  ralnex3  3113  nrexralim  3116  nrexdv  3127  nelb  3208  cbvrexdva  3213  cbvrexfw  3273  rexeqbidvvOLD  3303  cbvrexdva2  3315  rexeqf  3322  rexprg  4647  n0snor2el  4782  iindif2  5023  rexiunxp  5779  rexxpf  5786  f0rn0  6708  ordunisuc2  7774  tfi  7783  resf1extb  7864  releldmdifi  7977  omeulem1  8497  frfi  9169  isfinite2  9182  supmo  9336  infmo  9381  ordtypelem9  9412  elirrvOLD  9484  unbndrank  9735  kmlem7  10048  kmlem8  10049  kmlem13  10054  isfin1-3  10277  ac6num  10370  zorn2lem4  10390  fpwwe2lem11  10532  npomex  10887  suplem2pr  10944  dedekind  11276  suprnub  12087  infregelb  12106  arch  12378  xrsupsslem  13206  xrinfmsslem  13207  supxrbnd1  13220  supxrbnd2  13221  supxrleub  13225  supxrbnd  13227  infxrgelb  13235  injresinjlem  13690  hashgt12el  14329  hashgt12el2  14330  sqrt2irr  16158  prmind2  16596  vdwnnlem3  16909  vdwnn  16910  acsfiindd  18459  isnmnd  18646  isnirred  20338  lssne0  20884  bwth  23325  t1connperf  23351  trfbas  23759  fbunfip  23784  fbasrn  23799  filuni  23800  hausflim  23896  alexsubALTlem3  23964  alexsubALTlem4  23965  ptcmplem4  23970  lebnumlem3  24889  bcthlem4  25254  bcth3  25258  amgm  26928  issqf  27073  ostth  27577  nosupbnd1lem4  27650  noinfbnd1lem4  27665  sltrec  27762  cuteq1  27778  tglowdim2ln  28629  axcontlem12  28953  umgrnloop0  29087  numedglnl  29122  usgrnloop0ALT  29183  uhgrnbgr0nb  29332  nbgr0edg  29335  vtxd0nedgb  29467  vtxdusgr0edgnelALT  29475  1hevtxdg0  29484  usgrvd0nedg  29512  uhgrvd00  29513  pthdlem2lem  29745  nmounbi  30756  lnon0  30778  largei  32247  cvbr2  32263  chrelat2i  32345  n0nsnel  32495  uniinn0  32530  infxrge0gelb  32749  nn0min  32803  toslublem  32953  tosglblem  32955  archiabl  33167  lmdvg  33966  esumcvgre  34104  eulerpartlems  34373  bnj110  34870  bnj1417  35053  fineqvnttrclselem1  35141  lfuhgr3  35164  fmlaomn0  35434  fmla0disjsuc  35442  fmlasucdisj  35443  dfon2lem8  35832  dfint3  35996  relowlpssretop  37408  domalom  37448  fvineqsneq  37456  poimirlem26  37696  poimirlem30  37700  poimir  37703  mblfinlem1  37707  ftc1anc  37751  heiborlem1  37861  lcvbr2  39131  lcvbr3  39132  cvrnbtwn  39380  cvrval2  39383  hlrelat2  39512  cdleme0nex  40399  aks4d1p7  42186  sticksstones1  42249  infdesc  42746  nna4b4nsq  42763  rencldnfilem  42923  setindtr  43127  onmaxnelsup  43326  onsupnmax  43331  onsupmaxb  43342  onsupeqnmax  43350  ordnexbtwnsuc  43370  gneispace  44237  nelrnmpt  45191  iindif2f  45267  ralfal  45268  supxrgere  45442  supxrgelem  45446  infxrbnd2  45477  supminfxr  45572  limsupub  45812  limsuppnflem  45818  limsupre2lem  45832  stirlinglem5  46186  etransclem24  46366  etransclem32  46374  sge0iunmpt  46526  sge0rpcpnf  46529  iundjiun  46568  voliunsge0lem  46580  meaiuninc3v  46592  meaiininclem  46594  hoidmv1lelem3  46701  hoidmvlelem4  46706  hoidmvlelem5  46707  n0nsn2el  47135  0nelsetpreimafv  47500  stgr0  48070  gpg5nbgrvtx03starlem1  48178  gpg5nbgrvtx03starlem2  48179  gpg5nbgrvtx03starlem3  48180  gpg5nbgrvtx13starlem1  48181  gpg5nbgrvtx13starlem2  48182  gpg5nbgrvtx13starlem3  48183  gpg5edgnedg  48240  copisnmnd  48279  lindslinindsimp1  48568  lindslinindsimp2  48574  ldepslinc  48620  aacllem  49912