Theorem ralnex 3060

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 3057	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
2		alnex 1782	. . 3 ⊢ (∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ¬ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3		df-rex 3059	. . 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 2113  ∀wral 3049  ∃wrex 3058

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 3050  df-rex 3059

This theorem is referenced by:  dfrex2  3061  nrex  3062  rexim  3075  dfral2  3085  ralinexa  3087  r19.43  3102  ralnex2  3114  ralnex3  3115  nrexralim  3118  nrexdv  3129  nelb  3210  cbvrexdva  3215  cbvrexfw  3275  rexeqbidvvOLD  3305  cbvrexdva2  3317  rexeqf  3324  rexprg  4652  n0snor2el  4787  iindif2  5030  rexiunxp  5787  rexxpf  5794  nelrnmpt  5914  f0rn0  6717  ordunisuc2  7784  tfi  7793  resf1extb  7874  releldmdifi  7987  omeulem1  8507  frfi  9183  isfinite2  9196  supmo  9353  infmo  9398  ordtypelem9  9429  elirrvOLD  9501  unbndrank  9752  kmlem7  10065  kmlem8  10066  kmlem13  10071  isfin1-3  10294  ac6num  10387  zorn2lem4  10407  fpwwe2lem11  10550  npomex  10905  suplem2pr  10962  dedekind  11294  suprnub  12105  infregelb  12124  arch  12396  xrsupsslem  13220  xrinfmsslem  13221  supxrbnd1  13234  supxrbnd2  13235  supxrleub  13239  supxrbnd  13241  infxrgelb  13249  injresinjlem  13704  hashgt12el  14343  hashgt12el2  14344  sqrt2irr  16172  prmind2  16610  vdwnnlem3  16923  vdwnn  16924  acsfiindd  18474  isnmnd  18661  isnirred  20354  lssne0  20900  bwth  23352  t1connperf  23378  trfbas  23786  fbunfip  23811  fbasrn  23826  filuni  23827  hausflim  23923  alexsubALTlem3  23991  alexsubALTlem4  23992  ptcmplem4  23997  lebnumlem3  24916  bcthlem4  25281  bcth3  25285  amgm  26955  issqf  27100  ostth  27604  nosupbnd1lem4  27677  noinfbnd1lem4  27692  sltrec  27789  cuteq1  27805  tglowdim2ln  28672  axcontlem12  28997  umgrnloop0  29131  numedglnl  29166  usgrnloop0ALT  29227  uhgrnbgr0nb  29376  nbgr0edg  29379  vtxd0nedgb  29511  vtxdusgr0edgnelALT  29519  1hevtxdg0  29528  usgrvd0nedg  29556  uhgrvd00  29557  pthdlem2lem  29789  nmounbi  30800  lnon0  30822  largei  32291  cvbr2  32307  chrelat2i  32389  n0nsnel  32539  uniinn0  32574  infxrge0gelb  32795  nn0min  32850  toslublem  33003  tosglblem  33005  archiabl  33229  lmdvg  34059  esumcvgre  34197  eulerpartlems  34466  bnj110  34963  bnj1417  35146  fineqvnttrclselem1  35226  lfuhgr3  35263  fmlaomn0  35533  fmla0disjsuc  35541  fmlasucdisj  35542  dfon2lem8  35931  dfint3  36095  relowlpssretop  37508  domalom  37548  fvineqsneq  37556  poimirlem26  37786  poimirlem30  37790  poimir  37793  mblfinlem1  37797  ftc1anc  37841  heiborlem1  37951  lcvbr2  39221  lcvbr3  39222  cvrnbtwn  39470  cvrval2  39473  hlrelat2  39602  cdleme0nex  40489  aks4d1p7  42276  sticksstones1  42339  infdesc  42828  nna4b4nsq  42845  rencldnfilem  43004  setindtr  43208  onmaxnelsup  43407  onsupnmax  43412  onsupmaxb  43423  onsupeqnmax  43431  ordnexbtwnsuc  43451  gneispace  44317  iindif2f  45346  ralfal  45347  supxrgere  45520  supxrgelem  45524  infxrbnd2  45555  supminfxr  45650  limsupub  45890  limsuppnflem  45896  limsupre2lem  45910  stirlinglem5  46264  etransclem24  46444  etransclem32  46452  sge0iunmpt  46604  sge0rpcpnf  46607  iundjiun  46646  voliunsge0lem  46658  meaiuninc3v  46670  meaiininclem  46672  hoidmv1lelem3  46779  hoidmvlelem4  46784  hoidmvlelem5  46785  n0nsn2el  47213  0nelsetpreimafv  47578  stgr0  48148  gpg5nbgrvtx03starlem1  48256  gpg5nbgrvtx03starlem2  48257  gpg5nbgrvtx03starlem3  48258  gpg5nbgrvtx13starlem1  48259  gpg5nbgrvtx13starlem2  48260  gpg5nbgrvtx13starlem3  48261  gpg5edgnedg  48318  copisnmnd  48357  lindslinindsimp1  48645  lindslinindsimp2  48651  ldepslinc  48697  aacllem  49988