Theorem ralnex 3072

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 3069	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
2		alnex 1781	. . 3 ⊢ (∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ¬ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3		df-rex 3071	. . 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 2108  ∀wral 3061  ∃wrex 3070

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 3062  df-rex 3071

This theorem is referenced by:  dfrex2  3073  nrex  3074  rexim  3087  dfral2  3099  ralinexa  3101  r19.30OLD  3121  r19.43  3122  ralnex2  3133  ralnex3  3134  nrexralim  3137  nrexdv  3149  nelb  3234  nelbOLD  3235  cbvrexdva  3240  cbvrexfw  3305  rexeqbidvvOLD  3337  cbvrexdva2  3349  rexeqf  3354  rexprg  4697  n0snor2el  4833  iindif2  5077  rexiunxp  5851  rexxpf  5858  f0rn0  6793  ordunisuc2  7865  tfi  7874  resf1extb  7956  releldmdifi  8070  omeulem1  8620  frfi  9321  isfinite2  9334  supmo  9492  infmo  9535  ordtypelem9  9566  elirrv  9636  unbndrank  9882  kmlem7  10197  kmlem8  10198  kmlem13  10203  isfin1-3  10426  ac6num  10519  zorn2lem4  10539  fpwwe2lem11  10681  npomex  11036  suplem2pr  11093  dedekind  11424  suprnub  12233  infregelb  12252  arch  12523  xrsupsslem  13349  xrinfmsslem  13350  supxrbnd1  13363  supxrbnd2  13364  supxrleub  13368  supxrbnd  13370  infxrgelb  13377  injresinjlem  13826  hashgt12el  14461  hashgt12el2  14462  sqrt2irr  16285  prmind2  16722  vdwnnlem3  17035  vdwnn  17036  acsfiindd  18598  isnmnd  18751  isnirred  20420  lssne0  20949  bwth  23418  t1connperf  23444  trfbas  23852  fbunfip  23877  fbasrn  23892  filuni  23893  hausflim  23989  alexsubALTlem3  24057  alexsubALTlem4  24058  ptcmplem4  24063  lebnumlem3  24995  bcthlem4  25361  bcth3  25365  amgm  27034  issqf  27179  ostth  27683  nosupbnd1lem4  27756  noinfbnd1lem4  27771  sltrec  27865  cuteq1  27878  tglowdim2ln  28659  axcontlem12  28990  umgrnloop0  29126  numedglnl  29161  usgrnloop0ALT  29222  uhgrnbgr0nb  29371  nbgr0edg  29374  vtxd0nedgb  29506  vtxdusgr0edgnelALT  29514  1hevtxdg0  29523  usgrvd0nedg  29551  uhgrvd00  29552  pthdlem2lem  29787  nmounbi  30795  lnon0  30817  largei  32286  cvbr2  32302  chrelat2i  32384  n0nsnel  32534  uniinn0  32563  infxrge0gelb  32770  nn0min  32822  toslublem  32962  tosglblem  32964  archiabl  33205  lmdvg  33952  esumcvgre  34092  eulerpartlems  34362  bnj110  34872  bnj1417  35055  lfuhgr3  35125  fmlaomn0  35395  fmla0disjsuc  35403  fmlasucdisj  35404  dfon2lem8  35791  dfint3  35953  relowlpssretop  37365  domalom  37405  fvineqsneq  37413  poimirlem26  37653  poimirlem30  37657  poimir  37660  mblfinlem1  37664  ftc1anc  37708  heiborlem1  37818  lcvbr2  39023  lcvbr3  39024  cvrnbtwn  39272  cvrval2  39275  hlrelat2  39405  cdleme0nex  40292  aks4d1p7  42084  sticksstones1  42147  infdesc  42653  nna4b4nsq  42670  rencldnfilem  42831  setindtr  43036  onmaxnelsup  43235  onsupnmax  43240  onsupmaxb  43251  onsupeqnmax  43259  ordnexbtwnsuc  43280  gneispace  44147  nelrnmpt  45089  iindif2f  45165  ralfal  45166  supxrgere  45344  supxrgelem  45348  infxrbnd2  45380  supminfxr  45475  limsupub  45719  limsuppnflem  45725  limsupre2lem  45739  stirlinglem5  46093  etransclem24  46273  etransclem32  46281  sge0iunmpt  46433  sge0rpcpnf  46436  iundjiun  46475  voliunsge0lem  46487  meaiuninc3v  46499  meaiininclem  46501  hoidmv1lelem3  46608  hoidmvlelem4  46613  hoidmvlelem5  46614  n0nsn2el  47037  0nelsetpreimafv  47377  stgr0  47927  gpg5nbgrvtx03starlem1  48024  gpg5nbgrvtx03starlem2  48025  gpg5nbgrvtx03starlem3  48026  gpg5nbgrvtx13starlem1  48027  gpg5nbgrvtx13starlem2  48028  gpg5nbgrvtx13starlem3  48029  copisnmnd  48085  lindslinindsimp1  48374  lindslinindsimp2  48380  ldepslinc  48426  aacllem  49320