Theorem ralnex 3056

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 3053	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
2		alnex 1781	. . 3 ⊢ (∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ¬ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3		df-rex 3055	. . 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 2109  ∀wral 3045  ∃wrex 3054

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 3046  df-rex 3055

This theorem is referenced by:  dfrex2  3057  nrex  3058  rexim  3071  dfral2  3082  ralinexa  3084  r19.43  3102  ralnex2  3114  ralnex3  3115  nrexralim  3118  nrexdv  3129  nelb  3214  cbvrexdva  3219  cbvrexfw  3281  rexeqbidvvOLD  3312  cbvrexdva2  3324  rexeqf  3332  rexprg  4664  n0snor2el  4800  iindif2  5044  rexiunxp  5807  rexxpf  5814  f0rn0  6748  ordunisuc2  7823  tfi  7832  resf1extb  7913  releldmdifi  8027  omeulem1  8549  frfi  9239  isfinite2  9252  supmo  9410  infmo  9455  ordtypelem9  9486  elirrv  9556  unbndrank  9802  kmlem7  10117  kmlem8  10118  kmlem13  10123  isfin1-3  10346  ac6num  10439  zorn2lem4  10459  fpwwe2lem11  10601  npomex  10956  suplem2pr  11013  dedekind  11344  suprnub  12155  infregelb  12174  arch  12446  xrsupsslem  13274  xrinfmsslem  13275  supxrbnd1  13288  supxrbnd2  13289  supxrleub  13293  supxrbnd  13295  infxrgelb  13303  injresinjlem  13755  hashgt12el  14394  hashgt12el2  14395  sqrt2irr  16224  prmind2  16662  vdwnnlem3  16975  vdwnn  16976  acsfiindd  18519  isnmnd  18672  isnirred  20336  lssne0  20864  bwth  23304  t1connperf  23330  trfbas  23738  fbunfip  23763  fbasrn  23778  filuni  23779  hausflim  23875  alexsubALTlem3  23943  alexsubALTlem4  23944  ptcmplem4  23949  lebnumlem3  24869  bcthlem4  25234  bcth3  25238  amgm  26908  issqf  27053  ostth  27557  nosupbnd1lem4  27630  noinfbnd1lem4  27645  sltrec  27739  cuteq1  27753  tglowdim2ln  28585  axcontlem12  28909  umgrnloop0  29043  numedglnl  29078  usgrnloop0ALT  29139  uhgrnbgr0nb  29288  nbgr0edg  29291  vtxd0nedgb  29423  vtxdusgr0edgnelALT  29431  1hevtxdg0  29440  usgrvd0nedg  29468  uhgrvd00  29469  pthdlem2lem  29704  nmounbi  30712  lnon0  30734  largei  32203  cvbr2  32219  chrelat2i  32301  n0nsnel  32451  uniinn0  32486  infxrge0gelb  32696  nn0min  32752  toslublem  32905  tosglblem  32907  archiabl  33159  lmdvg  33950  esumcvgre  34088  eulerpartlems  34358  bnj110  34855  bnj1417  35038  lfuhgr3  35114  fmlaomn0  35384  fmla0disjsuc  35392  fmlasucdisj  35393  dfon2lem8  35785  dfint3  35947  relowlpssretop  37359  domalom  37399  fvineqsneq  37407  poimirlem26  37647  poimirlem30  37651  poimir  37654  mblfinlem1  37658  ftc1anc  37702  heiborlem1  37812  lcvbr2  39022  lcvbr3  39023  cvrnbtwn  39271  cvrval2  39274  hlrelat2  39404  cdleme0nex  40291  aks4d1p7  42078  sticksstones1  42141  infdesc  42638  nna4b4nsq  42655  rencldnfilem  42815  setindtr  43020  onmaxnelsup  43219  onsupnmax  43224  onsupmaxb  43235  onsupeqnmax  43243  ordnexbtwnsuc  43263  gneispace  44130  nelrnmpt  45085  iindif2f  45161  ralfal  45162  supxrgere  45336  supxrgelem  45340  infxrbnd2  45372  supminfxr  45467  limsupub  45709  limsuppnflem  45715  limsupre2lem  45729  stirlinglem5  46083  etransclem24  46263  etransclem32  46271  sge0iunmpt  46423  sge0rpcpnf  46426  iundjiun  46465  voliunsge0lem  46477  meaiuninc3v  46489  meaiininclem  46491  hoidmv1lelem3  46598  hoidmvlelem4  46603  hoidmvlelem5  46604  n0nsn2el  47030  0nelsetpreimafv  47395  stgr0  47963  gpg5nbgrvtx03starlem1  48063  gpg5nbgrvtx03starlem2  48064  gpg5nbgrvtx03starlem3  48065  gpg5nbgrvtx13starlem1  48066  gpg5nbgrvtx13starlem2  48067  gpg5nbgrvtx13starlem3  48068  copisnmnd  48161  lindslinindsimp1  48450  lindslinindsimp2  48456  ldepslinc  48502  aacllem  49794