Theorem ralnex 3073

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 3070	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
2		alnex 1782	. . 3 ⊢ (∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ¬ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3		df-rex 3072	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4	2, 3	xchbinxr 334	. 2 ⊢ (∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑)
5	1, 4	bitri 274	1 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 205   ∧ wa 396  ∀wal 1538  ∃wex 1780   ∈ wcel 2105  ∀wral 3062  ∃wrex 3071

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 206  df-an 397  df-ex 1781  df-ral 3063  df-rex 3072

This theorem is referenced by:  dfrex2  3074  nrex  3075  rexim  3087  dfral2  3099  ralinexa  3101  r19.30OLD  3121  r19.43  3122  ralnex2  3127  ralnex3  3128  nrexralim  3131  nrexdv  3143  nelb  3219  nelbOLD  3220  cbvrexfw  3285  rexeqbidvv  3303  cbvrexdva2  3321  rexprg  4640  n0snor2el  4774  iindif2  5017  rexiunxp  5767  rexxpf  5774  f0rn0  6694  ordunisuc2  7733  tfi  7742  releldmdifi  7929  omeulem1  8459  frfi  9127  isfinite2  9140  supmo  9279  infmo  9322  ordtypelem9  9353  elirrv  9423  unbndrank  9668  kmlem7  9982  kmlem8  9983  kmlem13  9988  isfin1-3  10212  ac6num  10305  zorn2lem4  10325  fpwwe2lem11  10467  npomex  10822  suplem2pr  10879  dedekind  11208  suprnub  12010  infregelb  12029  arch  12300  xrsupsslem  13111  xrinfmsslem  13112  supxrbnd1  13125  supxrbnd2  13126  supxrleub  13130  supxrbnd  13132  infxrgelb  13139  injresinjlem  13577  hashgt12el  14206  hashgt12el2  14207  sqrt2irr  16027  prmind2  16457  vdwnnlem3  16765  vdwnn  16766  acsfiindd  18338  isnmnd  18456  isnirred  20009  lssne0  20283  bwth  22632  t1connperf  22658  trfbas  23066  fbunfip  23091  fbasrn  23106  filuni  23107  hausflim  23203  alexsubALTlem3  23271  alexsubALTlem4  23272  ptcmplem4  23277  lebnumlem3  24197  bcthlem4  24562  bcth3  24566  amgm  26211  issqf  26356  ostth  26858  tglowdim2ln  27120  axcontlem12  27451  umgrnloop0  27587  numedglnl  27622  usgrnloop0ALT  27680  uhgrnbgr0nb  27829  nbgr0edg  27832  vtxd0nedgb  27963  vtxdusgr0edgnelALT  27971  1hevtxdg0  27980  usgrvd0nedg  28008  uhgrvd00  28009  pthdlem2lem  28243  nmounbi  29246  lnon0  29268  largei  30737  cvbr2  30753  chrelat2i  30835  uniinn0  30998  infxrge0gelb  31197  nn0min  31242  toslublem  31358  tosglblem  31360  archiabl  31560  lmdvg  32009  esumcvgre  32165  eulerpartlems  32433  bnj110  32944  bnj1417  33127  lfuhgr3  33187  fmlaomn0  33458  fmla0disjsuc  33466  fmlasucdisj  33467  dfon2lem8  33868  nosupbnd1lem4  33975  noinfbnd1lem4  33990  sltrec  34075  dfint3  34315  relowlpssretop  35595  domalom  35635  fvineqsneq  35643  poimirlem26  35863  poimirlem30  35867  poimir  35870  mblfinlem1  35874  ftc1anc  35918  heiborlem1  36029  lcvbr2  37248  lcvbr3  37249  cvrnbtwn  37497  cvrval2  37500  hlrelat2  37629  cdleme0nex  38516  aks4d1p7  40303  sticksstones1  40317  infdesc  40690  nna4b4nsq  40707  rencldnfilem  40852  setindtr  41057  gneispace  41972  nelrnmpt  42862  supxrgere  43115  supxrgelem  43119  infxrbnd2  43151  supminfxr  43247  limsupub  43489  limsuppnflem  43495  limsupre2lem  43509  stirlinglem5  43863  etransclem24  44043  etransclem32  44051  sge0iunmpt  44201  sge0rpcpnf  44204  iundjiun  44243  voliunsge0lem  44255  meaiuninc3v  44267  meaiininclem  44269  hoidmv1lelem3  44376  hoidmvlelem4  44381  hoidmvlelem5  44382  0nelsetpreimafv  45101  copisnmnd  45622  lindslinindsimp1  46057  lindslinindsimp2  46063  ldepslinc  46109  aacllem  46764