Theorem rexnal 3082

Description: Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.) (Proof shortened by Wolf Lammen, 9-Dec-2019.)

Assertion

Ref	Expression
rexnal	⊢ (∃𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 𝜑)

Proof of Theorem rexnal

Step	Hyp	Ref	Expression
1		dfral2 3081	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 ¬ 𝜑)
2	1	con2bii 357	1 ⊢ (∃𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wral 3044  ∃wrex 3053

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 3045  df-rex 3054

This theorem is referenced by:  r19.35  3088  r19.35OLD  3089  r19.30  3100  rexnal2  3115  rexnal3  3116  raleq  3296  elpwunsn  4648  n0snor2el  4797  uni0b  4897  iundif2  5038  weniso  7329  rexrnmpo  7529  onnseq  8313  cofonr  8638  ixp0  8904  boxcutc  8914  isfinite2  9245  ordtypelem9  9479  ordtypelem10  9480  unbndrank  9795  tcrank  9837  infxpenlem  9966  kmlem3  10106  kmlem7  10110  kmlem8  10111  kmlem13  10116  cfeq0  10209  isf32lem2  10307  isf32lem5  10310  isf34lem4  10330  fin1a2lem7  10359  ac6n  10438  alephval2  10525  pwfseqlem3  10613  inttsk  10727  nqereu  10882  npomex  10949  prlem934  10986  arch  12439  qextlt  13163  qextle  13164  xralrple  13165  xrsupsslem  13267  xrinfmsslem  13268  supxrbnd1  13281  supxrbnd2  13282  supxrbnd  13288  fsuppmapnn0fiubex  13957  hashfun  14402  hashge2el2dif  14445  limsuplt  15445  fprodle  15962  alzdvds  16290  isprm5  16677  ncoprmlnprm  16698  pc2dvds  16850  vdwnn  16969  ramcl  17000  cshwshashlem1  17066  cshwshash  17075  isnsgrp  18650  isnmnd  18665  smndex1n0mnd  18839  lt6abl  19825  simpgnideld  20031  zrninitoringc  20585  psdmul  22053  mdetunilem8  22506  fctop  22891  cctop  22893  t0dist  23212  ist0-3  23232  pthaus  23525  txkgen  23539  xkohaus  23540  fbfinnfr  23728  isufil2  23795  hausflim  23868  fclscf  23912  bcth  25229  minveclem3b  25328  pmltpc  25351  volsup  25457  volsup2  25506  itg2seq  25643  itg2cn  25664  tdeglem4  25965  aaliou3lem9  26258  ftalem7  26989  dchrptlem3  27177  dchrsum2  27179  noseponlem  27576  nolt02o  27607  noetasuplem4  27648  noetainflem4  27652  cofcutr  27832  tglowdim1i  28428  tglowdim2ln  28578  brbtwn2  28832  colinearalg  28837  axlowdimlem6  28874  axlowdimlem14  28882  umgr2edg1  29138  umgr2edgneu  29141  nfrgr2v  30201  4cycl2vnunb  30219  nmounbi  30705  nmobndseqi  30708  minvecolem5  30810  fprodex01  32750  xrnarchi  33138  isarchi2  33139  ssdifidllem  33427  mxidlirred  33443  ssmxidllem  33444  fedgmullem2  33626  ordtconnlem1  33914  lmdvg  33943  hasheuni  34075  voliune  34219  volfiniune  34220  ballotlemodife  34489  ballotlem4  34490  reprdifc  34618  bnj1542  34847  bnj110  34848  bnj1189  34999  dfrecs2  35938  brub  35942  filnetlem4  36369  unblimceq0  36495  relowlpssretop  37352  nlpineqsn  37396  matunitlindflem1  37610  poimirlem23  37637  poimirlem30  37644  poimirlem32  37646  poimir  37647  mblfinlem1  37651  aks4d1p3  42066  aks4d1p8d2  42073  aks6d1c2p2  42107  aks6d1c5  42127  dffltz  42622  infdesc  42631  fphpd  42804  fiphp3d  42807  rencldnfilem  42808  pellfundglb  42873  onmaxnelsup  43212  onsupnmax  43217  ralopabb  43400  clsk3nimkb  44029  ndisj2  45045  eliin2f  45098  infrpge  45347  infxrbnd2  45365  supminfxr  45460  rexanuz2nf  45488  limcrecl  45627  limsupub  45702  limsuppnflem  45708  limsupre2lem  45722  stoweidlem14  46012  stoweidlem34  46032  salexct  46332  meaiuninc3v  46482  vonioo  46680  vonicc  46683  tworepnotupword  46884  copisnmnd  48157  pgrpgt2nabl  48354  islindeps  48442  islininds2  48473  ldepslinc  48498  line2ylem  48740  line2xlem  48742  iineq0  48808  nelsubclem  49056  setc1onsubc  49591