Theorem ralnex 3236

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

Syntax hints:  ¬ wn 3   ↔ wb 208   ∧ wa 398  ∀wal 1535  ∃wex 1780   ∈ wcel 2114  ∀wral 3138  ∃wrex 3139

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 209  df-an 399  df-ex 1781  df-ral 3143  df-rex 3144

This theorem is referenced by:  dfral2  3237  dfrex2  3239  ralnex2  3260  ralnex3  3262  ralinexa  3264  nrexralim  3266  nelb  3268  nrex  3269  nrexdv  3270  r19.30  3338  r19.43  3351  n0snor2el  4764  iindif2  4999  rexiunxp  5711  rexxpf  5718  f0rn0  6564  ordunisuc2  7559  tfi  7568  releldmdifi  7744  omeulem1  8208  frfi  8763  isfinite2  8776  supmo  8916  infmo  8959  ordtypelem9  8990  elirrv  9060  unbndrank  9271  kmlem7  9582  kmlem8  9583  kmlem13  9588  isfin1-3  9808  ac6num  9901  zorn2lem4  9921  fpwwe2lem12  10063  npomex  10418  suplem2pr  10475  dedekind  10803  suprnub  11606  infregelb  11625  arch  11895  xrsupsslem  12701  xrinfmsslem  12702  supxrbnd1  12715  supxrbnd2  12716  supxrleub  12720  supxrbnd  12722  infxrgelb  12729  injresinjlem  13158  hashgt12el  13784  hashgt12el2  13785  sqrt2irr  15602  prmind2  16029  vdwnnlem3  16333  vdwnn  16334  acsfiindd  17787  isnmnd  17915  isnirred  19450  lssne0  19722  bwth  22018  t1connperf  22044  trfbas  22452  fbunfip  22477  fbasrn  22492  filuni  22493  hausflim  22589  alexsubALTlem3  22657  alexsubALTlem4  22658  ptcmplem4  22663  lebnumlem3  23567  bcthlem4  23930  bcth3  23934  amgm  25568  issqf  25713  ostth  26215  tglowdim2ln  26437  axcontlem12  26761  umgrnloop0  26894  numedglnl  26929  usgrnloop0ALT  26987  uhgrnbgr0nb  27136  nbgr0edg  27139  vtxd0nedgb  27270  vtxdusgr0edgnelALT  27278  1hevtxdg0  27287  usgrvd0nedg  27315  uhgrvd00  27316  pthdlem2lem  27548  nmounbi  28553  lnon0  28575  largei  30044  cvbr2  30060  chrelat2i  30142  uniinn0  30302  infxrge0gelb  30490  nn0min  30536  toslublem  30654  tosglblem  30656  archiabl  30827  lmdvg  31196  esumcvgre  31350  eulerpartlems  31618  bnj110  32130  bnj1417  32313  lfuhgr3  32366  fmlaomn0  32637  fmla0disjsuc  32645  fmlasucdisj  32646  dfon2lem8  33035  nosupbnd1lem4  33211  sltrec  33278  dfint3  33413  relowlpssretop  34648  domalom  34688  fvineqsneq  34696  poimirlem26  34933  poimirlem30  34937  poimir  34940  mblfinlem1  34944  ftc1anc  34990  heiborlem1  35104  lcvbr2  36173  lcvbr3  36174  cvrnbtwn  36422  cvrval2  36425  hlrelat2  36554  cdleme0nex  37441  rencldnfilem  39466  setindtr  39670  gneispace  40533  nelrnmpt  41397  supxrgere  41650  supxrgelem  41654  infxrbnd2  41686  supminfxr  41789  limsupub  42034  limsuppnflem  42040  limsupre2lem  42054  stirlinglem5  42412  etransclem24  42592  etransclem32  42600  sge0iunmpt  42749  sge0rpcpnf  42752  iundjiun  42791  voliunsge0lem  42803  meaiuninc3v  42815  meaiininclem  42817  hoidmv1lelem3  42924  hoidmvlelem4  42929  hoidmvlelem5  42930  0nelsetpreimafv  43599  copisnmnd  44125  lindslinindsimp1  44561  lindslinindsimp2  44567  ldepslinc  44613  aacllem  44951