Theorem rexnal 3169

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

Syntax hints:  ¬ wn 3   ↔ wb 205  ∀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:  rexnal2  3187  rexnal3  3188  r19.30  3268  r19.35  3271  2ralorOLD  3297  elpwunsn  4619  n0snor2el  4764  uni0b  4867  iundif2  5003  weniso  7225  rexrnmpo  7413  onnseq  8175  ixp0  8719  boxcutc  8729  isfinite2  9072  ordtypelem9  9285  ordtypelem10  9286  unbndrank  9600  tcrank  9642  infxpenlem  9769  kmlem3  9908  kmlem7  9912  kmlem8  9913  kmlem13  9918  cfeq0  10012  isf32lem2  10110  isf32lem5  10113  isf34lem4  10133  fin1a2lem7  10162  ac6n  10241  alephval2  10328  pwfseqlem3  10416  inttsk  10530  nqereu  10685  npomex  10752  prlem934  10789  arch  12230  qextlt  12937  qextle  12938  xralrple  12939  xrsupsslem  13041  xrinfmsslem  13042  supxrbnd1  13055  supxrbnd2  13056  supxrbnd  13062  fsuppmapnn0fiubex  13712  hashfun  14152  hashge2el2dif  14194  limsuplt  15188  fprodle  15706  alzdvds  16029  isprm5  16412  ncoprmlnprm  16432  pc2dvds  16580  vdwnn  16699  ramcl  16730  cshwshashlem1  16797  cshwshash  16806  isnsgrp  18379  isnmnd  18389  smndex1n0mnd  18551  lt6abl  19496  simpgnideld  19702  mdetunilem8  21768  fctop  22154  cctop  22156  t0dist  22476  ist0-3  22496  pthaus  22789  txkgen  22803  xkohaus  22804  fbfinnfr  22992  isufil2  23059  hausflim  23132  fclscf  23176  bcth  24493  minveclem3b  24592  pmltpc  24614  volsup  24720  volsup2  24769  itg2seq  24907  itg2cn  24928  tdeglem4  25224  tdeglem4OLD  25225  aaliou3lem9  25510  ftalem7  26228  dchrptlem3  26414  dchrsum2  26416  tglowdim1i  26862  tglowdim2ln  27012  brbtwn2  27273  colinearalg  27278  axlowdimlem6  27315  axlowdimlem14  27323  umgr2edg1  27578  umgr2edgneu  27581  nfrgr2v  28636  4cycl2vnunb  28654  nmounbi  29138  nmobndseqi  29141  minvecolem5  29243  fprodex01  31139  xrnarchi  31438  isarchi2  31439  ssmxidllem  31641  fedgmullem2  31711  ordtconnlem1  31874  lmdvg  31903  hasheuni  32053  voliune  32197  volfiniune  32198  ballotlemodife  32464  ballotlem4  32465  reprdifc  32607  bnj1542  32837  bnj110  32838  bnj1189  32989  noseponlem  33867  nolt02o  33898  noetasuplem4  33939  noetainflem4  33943  cofcutr  34092  dfrecs2  34252  brub  34256  filnetlem4  34570  unblimceq0  34687  relowlpssretop  35535  nlpineqsn  35579  matunitlindflem1  35773  poimirlem23  35800  poimirlem30  35807  poimirlem32  35809  poimir  35810  mblfinlem1  35814  aks4d1p3  40086  aks4d1p8d2  40093  dffltz  40471  infdesc  40480  fphpd  40638  fiphp3d  40641  rencldnfilem  40642  pellfundglb  40707  clsk3nimkb  41650  ndisj2  42599  eliin2f  42654  infrpge  42890  infxrbnd2  42908  supminfxr  43004  limcrecl  43170  limsupub  43245  limsuppnflem  43251  limsupre2lem  43265  stoweidlem14  43555  stoweidlem34  43575  salexct  43873  meaiuninc3v  44022  vonioo  44220  vonicc  44223  copisnmnd  45363  zrninitoringc  45629  pgrpgt2nabl  45702  islindeps  45794  islininds2  45825  ldepslinc  45850  line2ylem  46097  line2xlem  46099  tworepnotupword  46521