Theorem rexnal 3240

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 3239	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 ¬ 𝜑)
2	1	con2bii 360	1 ⊢ (∃𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 208  ∀wral 3140  ∃wrex 3141

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 209  df-an 399  df-ex 1781  df-ral 3145  df-rex 3146

This theorem is referenced by:  rexnal2  3260  rexnal3  3261  r19.35  3343  2ralor  3371  elpwunsn  4623  n0snor2el  4766  uni0b  4866  iundif2  4998  weniso  7109  rexrnmpo  7292  onnseq  7983  ixp0  8497  boxcutc  8507  isfinite2  8778  ordtypelem9  8992  ordtypelem10  8993  unbndrank  9273  tcrank  9315  infxpenlem  9441  kmlem3  9580  kmlem7  9584  kmlem8  9585  kmlem13  9590  cfeq0  9680  isf32lem2  9778  isf32lem5  9781  isf34lem4  9801  fin1a2lem7  9830  ac6n  9909  alephval2  9996  pwfseqlem3  10084  inttsk  10198  nqereu  10353  npomex  10420  prlem934  10457  arch  11897  qextlt  12599  qextle  12600  xralrple  12601  xrsupsslem  12703  xrinfmsslem  12704  supxrbnd1  12717  supxrbnd2  12718  supxrbnd  12724  fsuppmapnn0fiubex  13363  hashfun  13801  hashge2el2dif  13841  limsuplt  14838  fprodle  15352  alzdvds  15672  isprm5  16053  ncoprmlnprm  16070  pc2dvds  16217  vdwnn  16336  ramcl  16367  cshwshashlem1  16431  cshwshash  16440  isnsgrp  17907  isnmnd  17917  smndex1n0mnd  18079  lt6abl  19017  simpgnideld  19223  mdetunilem8  21230  fctop  21614  cctop  21616  t0dist  21935  ist0-3  21955  pthaus  22248  txkgen  22262  xkohaus  22263  fbfinnfr  22451  isufil2  22518  hausflim  22591  fclscf  22635  bcth  23934  minveclem3b  24033  pmltpc  24053  volsup  24159  volsup2  24208  itg2seq  24345  itg2cn  24366  tdeglem4  24656  aaliou3lem9  24941  ftalem7  25658  dchrptlem3  25844  dchrsum2  25846  tglowdim1i  26289  tglowdim2ln  26439  brbtwn2  26693  colinearalg  26698  axlowdimlem6  26735  axlowdimlem14  26743  umgr2edg1  26995  umgr2edgneu  26998  nfrgr2v  28053  4cycl2vnunb  28071  nmounbi  28555  nmobndseqi  28558  minvecolem5  28660  fprodex01  30543  xrnarchi  30815  isarchi2  30816  ssmxidllem  30980  fedgmullem2  31028  ordtconnlem1  31169  lmdvg  31198  hasheuni  31346  voliune  31490  volfiniune  31491  ballotlemodife  31757  ballotlem4  31758  reprdifc  31900  bnj1542  32131  bnj110  32132  bnj1189  32283  noseponlem  33173  nolt02o  33201  noetalem3  33221  dfrecs2  33413  brub  33417  filnetlem4  33731  unblimceq0  33848  relowlpssretop  34647  nlpineqsn  34691  matunitlindflem1  34890  poimirlem23  34917  poimirlem30  34924  poimirlem32  34926  poimir  34927  mblfinlem1  34931  dffltz  39278  fphpd  39420  fiphp3d  39423  rencldnfilem  39424  pellfundglb  39489  clsk3nimkb  40397  ndisj2  41320  eliin2f  41377  infrpge  41626  infxrbnd2  41644  supminfxr  41747  limcrecl  41917  limsupub  41992  limsuppnflem  41998  limsupre2lem  42012  stoweidlem14  42306  stoweidlem34  42326  salexct  42624  meaiuninc3v  42773  vonioo  42971  vonicc  42974  copisnmnd  44083  zrninitoringc  44349  pgrpgt2nabl  44421  islindeps  44515  islininds2  44546  ldepslinc  44571  line2ylem  44745  line2xlem  44747