Theorem ralnex 3167

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

Syntax hints:  ¬ wn 3   ↔ wb 205   ∧ wa 396  ∀wal 1537  ∃wex 1782   ∈ wcel 2106  ∀wral 3064  ∃wrex 3065

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-ral 3069  df-rex 3070

This theorem is referenced by:  dfral2  3168  dfrex2  3170  rexim  3172  ralnex2  3189  ralnex3  3190  ralinexa  3191  nrexralim  3193  nelb  3195  nelbOLD  3196  nrex  3197  nrexdv  3198  r19.30OLD  3269  r19.43  3280  rexeqbidvv  3339  cbvrexfw  3370  rexprg  4632  n0snor2el  4764  iindif2  5006  rexiunxp  5749  rexxpf  5756  f0rn0  6659  ordunisuc2  7691  tfi  7700  releldmdifi  7886  omeulem1  8413  frfi  9059  isfinite2  9072  supmo  9211  infmo  9254  ordtypelem9  9285  elirrv  9355  unbndrank  9600  kmlem7  9912  kmlem8  9913  kmlem13  9918  isfin1-3  10142  ac6num  10235  zorn2lem4  10255  fpwwe2lem11  10397  npomex  10752  suplem2pr  10809  dedekind  11138  suprnub  11940  infregelb  11959  arch  12230  xrsupsslem  13041  xrinfmsslem  13042  supxrbnd1  13055  supxrbnd2  13056  supxrleub  13060  supxrbnd  13062  infxrgelb  13069  injresinjlem  13507  hashgt12el  14137  hashgt12el2  14138  sqrt2irr  15958  prmind2  16390  vdwnnlem3  16698  vdwnn  16699  acsfiindd  18271  isnmnd  18389  isnirred  19942  lssne0  20212  bwth  22561  t1connperf  22587  trfbas  22995  fbunfip  23020  fbasrn  23035  filuni  23036  hausflim  23132  alexsubALTlem3  23200  alexsubALTlem4  23201  ptcmplem4  23206  lebnumlem3  24126  bcthlem4  24491  bcth3  24495  amgm  26140  issqf  26285  ostth  26787  tglowdim2ln  27012  axcontlem12  27343  umgrnloop0  27479  numedglnl  27514  usgrnloop0ALT  27572  uhgrnbgr0nb  27721  nbgr0edg  27724  vtxd0nedgb  27855  vtxdusgr0edgnelALT  27863  1hevtxdg0  27872  usgrvd0nedg  27900  uhgrvd00  27901  pthdlem2lem  28135  nmounbi  29138  lnon0  29160  largei  30629  cvbr2  30645  chrelat2i  30727  uniinn0  30890  infxrge0gelb  31089  nn0min  31134  toslublem  31250  tosglblem  31252  archiabl  31452  lmdvg  31903  esumcvgre  32059  eulerpartlems  32327  bnj110  32838  bnj1417  33021  lfuhgr3  33081  fmlaomn0  33352  fmla0disjsuc  33360  fmlasucdisj  33361  dfon2lem8  33766  nosupbnd1lem4  33914  noinfbnd1lem4  33929  sltrec  34014  dfint3  34254  relowlpssretop  35535  domalom  35575  fvineqsneq  35583  poimirlem26  35803  poimirlem30  35807  poimir  35810  mblfinlem1  35814  ftc1anc  35858  heiborlem1  35969  lcvbr2  37036  lcvbr3  37037  cvrnbtwn  37285  cvrval2  37288  hlrelat2  37417  cdleme0nex  38304  aks4d1p7  40091  sticksstones1  40102  infdesc  40480  nna4b4nsq  40497  rencldnfilem  40642  setindtr  40846  gneispace  41744  nelrnmpt  42634  supxrgere  42872  supxrgelem  42876  infxrbnd2  42908  supminfxr  43004  limsupub  43245  limsuppnflem  43251  limsupre2lem  43265  stirlinglem5  43619  etransclem24  43799  etransclem32  43807  sge0iunmpt  43956  sge0rpcpnf  43959  iundjiun  43998  voliunsge0lem  44010  meaiuninc3v  44022  meaiininclem  44024  hoidmv1lelem3  44131  hoidmvlelem4  44136  hoidmvlelem5  44137  0nelsetpreimafv  44842  copisnmnd  45363  lindslinindsimp1  45798  lindslinindsimp2  45804  ldepslinc  45850  aacllem  46505