Theorem rexnal 3100

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

Syntax hints:  ¬ wn 3   ↔ wb 205  ∀wral 3061  ∃wrex 3070

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-ral 3062  df-rex 3071

This theorem is referenced by:  r19.35  3108  r19.35OLD  3109  r19.30  3120  rexnal2  3135  rexnal3  3136  2ralorOLD  3229  raleq  3322  elpwunsn  4687  n0snor2el  4834  uni0b  4937  iundif2  5077  weniso  7353  rexrnmpo  7550  onnseq  8346  cofonr  8675  ixp0  8927  boxcutc  8937  isfinite2  9303  ordtypelem9  9523  ordtypelem10  9524  unbndrank  9839  tcrank  9881  infxpenlem  10010  kmlem3  10149  kmlem7  10153  kmlem8  10154  kmlem13  10159  cfeq0  10253  isf32lem2  10351  isf32lem5  10354  isf34lem4  10374  fin1a2lem7  10403  ac6n  10482  alephval2  10569  pwfseqlem3  10657  inttsk  10771  nqereu  10926  npomex  10993  prlem934  11030  arch  12473  qextlt  13186  qextle  13187  xralrple  13188  xrsupsslem  13290  xrinfmsslem  13291  supxrbnd1  13304  supxrbnd2  13305  supxrbnd  13311  fsuppmapnn0fiubex  13961  hashfun  14401  hashge2el2dif  14445  limsuplt  15427  fprodle  15944  alzdvds  16267  isprm5  16648  ncoprmlnprm  16668  pc2dvds  16816  vdwnn  16935  ramcl  16966  cshwshashlem1  17033  cshwshash  17042  isnsgrp  18648  isnmnd  18663  smndex1n0mnd  18829  lt6abl  19804  simpgnideld  20010  mdetunilem8  22341  fctop  22727  cctop  22729  t0dist  23049  ist0-3  23069  pthaus  23362  txkgen  23376  xkohaus  23377  fbfinnfr  23565  isufil2  23632  hausflim  23705  fclscf  23749  bcth  25070  minveclem3b  25169  pmltpc  25191  volsup  25297  volsup2  25346  itg2seq  25484  itg2cn  25505  tdeglem4  25801  tdeglem4OLD  25802  aaliou3lem9  26087  ftalem7  26807  dchrptlem3  26993  dchrsum2  26995  noseponlem  27391  nolt02o  27422  noetasuplem4  27463  noetainflem4  27467  cofcutr  27637  tglowdim1i  28007  tglowdim2ln  28157  brbtwn2  28418  colinearalg  28423  axlowdimlem6  28460  axlowdimlem14  28468  umgr2edg1  28723  umgr2edgneu  28726  nfrgr2v  29780  4cycl2vnunb  29798  nmounbi  30284  nmobndseqi  30287  minvecolem5  30389  fprodex01  32286  xrnarchi  32588  isarchi2  32589  mxidlirred  32850  ssmxidllem  32851  fedgmullem2  32991  ordtconnlem1  33190  lmdvg  33219  hasheuni  33369  voliune  33513  volfiniune  33514  ballotlemodife  33782  ballotlem4  33783  reprdifc  33925  bnj1542  34154  bnj110  34155  bnj1189  34306  dfrecs2  35214  brub  35218  filnetlem4  35569  unblimceq0  35686  relowlpssretop  36548  nlpineqsn  36592  matunitlindflem1  36787  poimirlem23  36814  poimirlem30  36821  poimirlem32  36823  poimir  36824  mblfinlem1  36828  aks4d1p3  41249  aks4d1p8d2  41256  aks6d1c2p2  41263  dffltz  41678  infdesc  41687  fphpd  41856  fiphp3d  41859  rencldnfilem  41860  pellfundglb  41925  onmaxnelsup  42274  onsupnmax  42279  ralopabb  42464  clsk3nimkb  43093  ndisj2  44040  eliin2f  44095  infrpge  44360  infxrbnd2  44378  supminfxr  44473  rexanuz2nf  44502  limcrecl  44644  limsupub  44719  limsuppnflem  44725  limsupre2lem  44739  stoweidlem14  45029  stoweidlem34  45049  salexct  45349  meaiuninc3v  45499  vonioo  45697  vonicc  45700  tworepnotupword  45899  copisnmnd  46846  zrninitoringc  47058  pgrpgt2nabl  47131  islindeps  47222  islininds2  47253  ldepslinc  47278  line2ylem  47525  line2xlem  47527