Theorem ralnex 3064

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 3061	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
2		alnex 1783	. . 3 ⊢ (∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ¬ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3		df-rex 3063	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4	2, 3	xchbinxr 335	. 2 ⊢ (∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑)
5	1, 4	bitri 275	1 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395  ∀wal 1540  ∃wex 1781   ∈ wcel 2114  ∀wral 3052  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-ral 3053  df-rex 3063

This theorem is referenced by:  dfrex2  3065  nrex  3066  rexim  3079  dfral2  3089  ralinexa  3091  r19.43  3106  ralnex2  3118  ralnex3  3119  nrexralim  3122  nrexdv  3133  nelb  3214  cbvrexdva  3219  cbvrexfw  3279  cbvrexdva2  3315  rexeqf  3320  rexprg  4642  n0snor2el  4777  iindif2  5020  rexiunxp  5790  rexxpf  5797  nelrnmpt  5917  f0rn0  6720  ordunisuc2  7789  tfi  7798  resf1extb  7879  releldmdifi  7992  omeulem1  8511  frfi  9189  isfinite2  9202  supmo  9359  infmo  9404  ordtypelem9  9435  elirrvOLD  9507  unbndrank  9760  kmlem7  10073  kmlem8  10074  kmlem13  10079  isfin1-3  10302  ac6num  10395  zorn2lem4  10415  fpwwe2lem11  10558  npomex  10913  suplem2pr  10970  dedekind  11303  suprnub  12115  infregelb  12134  arch  12428  xrsupsslem  13253  xrinfmsslem  13254  supxrbnd1  13267  supxrbnd2  13268  supxrleub  13272  supxrbnd  13274  infxrgelb  13282  injresinjlem  13739  hashgt12el  14378  hashgt12el2  14379  sqrt2irr  16210  prmind2  16648  vdwnnlem3  16962  vdwnn  16963  acsfiindd  18513  isnmnd  18700  isnirred  20394  lssne0  20940  bwth  23388  t1connperf  23414  trfbas  23822  fbunfip  23847  fbasrn  23862  filuni  23863  hausflim  23959  alexsubALTlem3  24027  alexsubALTlem4  24028  ptcmplem4  24033  lebnumlem3  24943  bcthlem4  25307  bcth3  25311  amgm  26971  issqf  27116  ostth  27619  nosupbnd1lem4  27692  noinfbnd1lem4  27707  ltsrec  27810  cuteq1  27826  tglowdim2ln  28736  axcontlem12  29061  umgrnloop0  29195  numedglnl  29230  usgrnloop0ALT  29291  uhgrnbgr0nb  29440  nbgr0edg  29443  vtxd0nedgb  29575  vtxdusgr0edgnelALT  29583  1hevtxdg0  29592  usgrvd0nedg  29620  uhgrvd00  29621  pthdlem2lem  29853  nmounbi  30865  lnon0  30887  largei  32356  cvbr2  32372  chrelat2i  32454  n0nsnel  32603  uniinn0  32638  infxrge0gelb  32857  nn0min  32912  toslublem  33050  tosglblem  33052  archiabl  33277  lmdvg  34116  esumcvgre  34254  eulerpartlems  34523  bnj110  35019  bnj1417  35202  fineqvnttrclselem1  35284  lfuhgr3  35321  fmlaomn0  35591  fmla0disjsuc  35599  fmlasucdisj  35600  dfon2lem8  35989  dfint3  36153  bj-axseprep  37400  relowlpssretop  37697  domalom  37737  fvineqsneq  37745  poimirlem26  37984  poimirlem30  37988  poimir  37991  mblfinlem1  37995  ftc1anc  38039  heiborlem1  38149  lcvbr2  39485  lcvbr3  39486  cvrnbtwn  39734  cvrval2  39737  hlrelat2  39866  cdleme0nex  40753  aks4d1p7  42539  sticksstones1  42602  infdesc  43093  nna4b4nsq  43110  rencldnfilem  43269  setindtr  43473  onmaxnelsup  43672  onsupnmax  43677  onsupmaxb  43688  onsupeqnmax  43696  ordnexbtwnsuc  43716  gneispace  44582  iindif2f  45611  ralfal  45612  supxrgere  45784  supxrgelem  45788  infxrbnd2  45819  supminfxr  45913  limsupub  46153  limsuppnflem  46159  limsupre2lem  46173  stirlinglem5  46527  etransclem24  46707  etransclem32  46715  sge0iunmpt  46867  sge0rpcpnf  46870  iundjiun  46909  voliunsge0lem  46921  meaiuninc3v  46933  meaiininclem  46935  hoidmv1lelem3  47042  hoidmvlelem4  47047  hoidmvlelem5  47048  n0nsn2el  47488  0nelsetpreimafv  47865  nprmmul1  48002  stgr0  48451  gpg5nbgrvtx03starlem1  48559  gpg5nbgrvtx03starlem2  48560  gpg5nbgrvtx03starlem3  48561  gpg5nbgrvtx13starlem1  48562  gpg5nbgrvtx13starlem2  48563  gpg5nbgrvtx13starlem3  48564  gpg5edgnedg  48621  copisnmnd  48660  lindslinindsimp1  48948  lindslinindsimp2  48954  ldepslinc  49000  aacllem  50291