Theorem ralnex 3062

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 3059	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
2		alnex 1782	. . 3 ⊢ (∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ¬ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3		df-rex 3061	. . 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 3051  ∃wrex 3060

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 3052  df-rex 3061

This theorem is referenced by:  dfrex2  3063  nrex  3064  rexim  3077  dfral2  3087  ralinexa  3089  r19.43  3104  ralnex2  3116  ralnex3  3117  nrexralim  3120  nrexdv  3131  nelb  3212  cbvrexdva  3217  cbvrexfw  3277  rexeqbidvvOLD  3307  cbvrexdva2  3319  rexeqf  3326  rexprg  4654  n0snor2el  4789  iindif2  5032  rexiunxp  5789  rexxpf  5796  nelrnmpt  5916  f0rn0  6719  ordunisuc2  7786  tfi  7795  resf1extb  7876  releldmdifi  7989  omeulem1  8509  frfi  9187  isfinite2  9200  supmo  9357  infmo  9402  ordtypelem9  9433  elirrvOLD  9505  unbndrank  9756  kmlem7  10069  kmlem8  10070  kmlem13  10075  isfin1-3  10298  ac6num  10391  zorn2lem4  10411  fpwwe2lem11  10554  npomex  10909  suplem2pr  10966  dedekind  11298  suprnub  12109  infregelb  12128  arch  12400  xrsupsslem  13224  xrinfmsslem  13225  supxrbnd1  13238  supxrbnd2  13239  supxrleub  13243  supxrbnd  13245  infxrgelb  13253  injresinjlem  13708  hashgt12el  14347  hashgt12el2  14348  sqrt2irr  16176  prmind2  16614  vdwnnlem3  16927  vdwnn  16928  acsfiindd  18478  isnmnd  18665  isnirred  20358  lssne0  20904  bwth  23356  t1connperf  23382  trfbas  23790  fbunfip  23815  fbasrn  23830  filuni  23831  hausflim  23927  alexsubALTlem3  23995  alexsubALTlem4  23996  ptcmplem4  24001  lebnumlem3  24920  bcthlem4  25285  bcth3  25289  amgm  26959  issqf  27104  ostth  27608  nosupbnd1lem4  27681  noinfbnd1lem4  27696  ltsrec  27799  cuteq1  27815  tglowdim2ln  28725  axcontlem12  29050  umgrnloop0  29184  numedglnl  29219  usgrnloop0ALT  29280  uhgrnbgr0nb  29429  nbgr0edg  29432  vtxd0nedgb  29564  vtxdusgr0edgnelALT  29572  1hevtxdg0  29581  usgrvd0nedg  29609  uhgrvd00  29610  pthdlem2lem  29842  nmounbi  30853  lnon0  30875  largei  32344  cvbr2  32360  chrelat2i  32442  n0nsnel  32592  uniinn0  32627  infxrge0gelb  32848  nn0min  32903  toslublem  33056  tosglblem  33058  archiabl  33282  lmdvg  34112  esumcvgre  34250  eulerpartlems  34519  bnj110  35016  bnj1417  35199  fineqvnttrclselem1  35279  lfuhgr3  35316  fmlaomn0  35586  fmla0disjsuc  35594  fmlasucdisj  35595  dfon2lem8  35984  dfint3  36148  relowlpssretop  37571  domalom  37611  fvineqsneq  37619  poimirlem26  37849  poimirlem30  37853  poimir  37856  mblfinlem1  37860  ftc1anc  37904  heiborlem1  38014  lcvbr2  39304  lcvbr3  39305  cvrnbtwn  39553  cvrval2  39556  hlrelat2  39685  cdleme0nex  40572  aks4d1p7  42359  sticksstones1  42422  infdesc  42907  nna4b4nsq  42924  rencldnfilem  43083  setindtr  43287  onmaxnelsup  43486  onsupnmax  43491  onsupmaxb  43502  onsupeqnmax  43510  ordnexbtwnsuc  43530  gneispace  44396  iindif2f  45425  ralfal  45426  supxrgere  45599  supxrgelem  45603  infxrbnd2  45634  supminfxr  45729  limsupub  45969  limsuppnflem  45975  limsupre2lem  45989  stirlinglem5  46343  etransclem24  46523  etransclem32  46531  sge0iunmpt  46683  sge0rpcpnf  46686  iundjiun  46725  voliunsge0lem  46737  meaiuninc3v  46749  meaiininclem  46751  hoidmv1lelem3  46858  hoidmvlelem4  46863  hoidmvlelem5  46864  n0nsn2el  47292  0nelsetpreimafv  47657  stgr0  48227  gpg5nbgrvtx03starlem1  48335  gpg5nbgrvtx03starlem2  48336  gpg5nbgrvtx03starlem3  48337  gpg5nbgrvtx13starlem1  48338  gpg5nbgrvtx13starlem2  48339  gpg5nbgrvtx13starlem3  48340  gpg5edgnedg  48397  copisnmnd  48436  lindslinindsimp1  48724  lindslinindsimp2  48730  ldepslinc  48776  aacllem  50067