Theorem ralnex 3239

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

Syntax hints:  ¬ wn 3   ↔ wb 208   ∧ wa 398  ∀wal 1534  ∃wex 1779   ∈ wcel 2113  ∀wral 3141  ∃wrex 3142

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 209  df-an 399  df-ex 1780  df-ral 3146  df-rex 3147

This theorem is referenced by:  dfral2  3240  dfrex2  3242  ralnex2  3263  ralnex3  3265  ralinexa  3267  nrexralim  3269  nelb  3271  nrex  3272  nrexdv  3273  r19.30  3341  r19.43  3354  n0snor2el  4767  iindif2  5002  rexiunxp  5714  rexxpf  5721  f0rn0  6567  ordunisuc2  7562  tfi  7571  releldmdifi  7747  omeulem1  8211  frfi  8766  isfinite2  8779  supmo  8919  infmo  8962  ordtypelem9  8993  elirrv  9063  unbndrank  9274  kmlem7  9585  kmlem8  9586  kmlem13  9591  isfin1-3  9811  ac6num  9904  zorn2lem4  9924  fpwwe2lem12  10066  npomex  10421  suplem2pr  10478  dedekind  10806  suprnub  11609  infregelb  11628  arch  11897  xrsupsslem  12703  xrinfmsslem  12704  supxrbnd1  12717  supxrbnd2  12718  supxrleub  12722  supxrbnd  12724  infxrgelb  12731  injresinjlem  13160  hashgt12el  13786  hashgt12el2  13787  sqrt2irr  15605  prmind2  16032  vdwnnlem3  16336  vdwnn  16337  acsfiindd  17790  isnmnd  17918  isnirred  19453  lssne0  19725  bwth  22021  t1connperf  22047  trfbas  22455  fbunfip  22480  fbasrn  22495  filuni  22496  hausflim  22592  alexsubALTlem3  22660  alexsubALTlem4  22661  ptcmplem4  22666  lebnumlem3  23570  bcthlem4  23933  bcth3  23937  amgm  25571  issqf  25716  ostth  26218  tglowdim2ln  26440  axcontlem12  26764  umgrnloop0  26897  numedglnl  26932  usgrnloop0ALT  26990  uhgrnbgr0nb  27139  nbgr0edg  27142  vtxd0nedgb  27273  vtxdusgr0edgnelALT  27281  1hevtxdg0  27290  usgrvd0nedg  27318  uhgrvd00  27319  pthdlem2lem  27551  nmounbi  28556  lnon0  28578  largei  30047  cvbr2  30063  chrelat2i  30145  uniinn0  30305  infxrge0gelb  30493  nn0min  30540  toslublem  30658  tosglblem  30660  archiabl  30831  lmdvg  31200  esumcvgre  31354  eulerpartlems  31622  bnj110  32134  bnj1417  32317  lfuhgr3  32370  fmlaomn0  32641  fmla0disjsuc  32649  fmlasucdisj  32650  dfon2lem8  33039  nosupbnd1lem4  33215  sltrec  33282  dfint3  33417  relowlpssretop  34649  domalom  34689  fvineqsneq  34697  poimirlem26  34922  poimirlem30  34926  poimir  34929  mblfinlem1  34933  ftc1anc  34979  heiborlem1  35093  lcvbr2  36162  lcvbr3  36163  cvrnbtwn  36411  cvrval2  36414  hlrelat2  36543  cdleme0nex  37430  rencldnfilem  39423  setindtr  39627  gneispace  40490  nelrnmpt  41354  supxrgere  41607  supxrgelem  41611  infxrbnd2  41643  supminfxr  41746  limsupub  41991  limsuppnflem  41997  limsupre2lem  42011  stirlinglem5  42370  etransclem24  42550  etransclem32  42558  sge0iunmpt  42707  sge0rpcpnf  42710  iundjiun  42749  voliunsge0lem  42761  meaiuninc3v  42773  meaiininclem  42775  hoidmv1lelem3  42882  hoidmvlelem4  42887  hoidmvlelem5  42888  0nelsetpreimafv  43557  copisnmnd  44083  lindslinindsimp1  44519  lindslinindsimp2  44525  ldepslinc  44571  aacllem  44909