Theorem rexnal 3093

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

Syntax hints:  ¬ wn 3   ↔ wb 205  ∀wral 3054  ∃wrex 3063

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

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-ral 3055  df-rex 3064

This theorem is referenced by:  r19.35  3101  r19.35OLD  3102  r19.30  3113  rexnal2  3128  rexnal3  3129  2ralorOLD  3224  raleq  3316  elpwunsn  4693  n0snor2el  4843  uni0b  4944  iundif2  5085  weniso  7369  rexrnmpo  7568  onnseq  8378  cofonr  8708  ixp0  8964  boxcutc  8974  isfinite2  9337  ordtypelem9  9570  ordtypelem10  9571  unbndrank  9886  tcrank  9928  infxpenlem  10057  kmlem3  10197  kmlem7  10201  kmlem8  10202  kmlem13  10207  cfeq0  10300  isf32lem2  10398  isf32lem5  10401  isf34lem4  10421  fin1a2lem7  10450  ac6n  10529  alephval2  10616  pwfseqlem3  10704  inttsk  10818  nqereu  10973  npomex  11040  prlem934  11077  arch  12525  qextlt  13240  qextle  13241  xralrple  13242  xrsupsslem  13344  xrinfmsslem  13345  supxrbnd1  13358  supxrbnd2  13359  supxrbnd  13365  fsuppmapnn0fiubex  14017  hashfun  14460  hashge2el2dif  14503  limsuplt  15494  fprodle  16011  alzdvds  16335  isprm5  16721  ncoprmlnprm  16743  pc2dvds  16894  vdwnn  17013  ramcl  17044  cshwshashlem1  17111  cshwshash  17120  isnsgrp  18729  isnmnd  18744  smndex1n0mnd  18915  lt6abl  19905  simpgnideld  20111  zrninitoringc  20666  psdmul  22159  mdetunilem8  22612  fctop  22998  cctop  23000  t0dist  23320  ist0-3  23340  pthaus  23633  txkgen  23647  xkohaus  23648  fbfinnfr  23836  isufil2  23903  hausflim  23976  fclscf  24020  bcth  25348  minveclem3b  25447  pmltpc  25470  volsup  25576  volsup2  25625  itg2seq  25763  itg2cn  25784  tdeglem4  26084  aaliou3lem9  26375  ftalem7  27104  dchrptlem3  27292  dchrsum2  27294  noseponlem  27691  nolt02o  27722  noetasuplem4  27763  noetainflem4  27767  cofcutr  27938  tglowdim1i  28470  tglowdim2ln  28620  brbtwn2  28881  colinearalg  28886  axlowdimlem6  28923  axlowdimlem14  28931  umgr2edg1  29189  umgr2edgneu  29192  nfrgr2v  30247  4cycl2vnunb  30265  nmounbi  30751  nmobndseqi  30754  minvecolem5  30856  fprodex01  32774  xrnarchi  33109  isarchi2  33110  ssdifidllem  33394  mxidlirred  33410  ssmxidllem  33411  fedgmullem2  33588  ordtconnlem1  33815  lmdvg  33844  hasheuni  33994  voliune  34138  volfiniune  34139  ballotlemodife  34407  ballotlem4  34408  reprdifc  34549  bnj1542  34778  bnj110  34779  bnj1189  34930  dfrecs2  35859  brub  35863  filnetlem4  36179  unblimceq0  36296  relowlpssretop  37156  nlpineqsn  37200  matunitlindflem1  37402  poimirlem23  37429  poimirlem30  37436  poimirlem32  37438  poimir  37439  mblfinlem1  37443  aks4d1p3  41862  aks4d1p8d2  41869  aks6d1c2p2  41903  aks6d1c5  41923  dffltz  42399  infdesc  42408  fphpd  42585  fiphp3d  42588  rencldnfilem  42589  pellfundglb  42654  onmaxnelsup  43000  onsupnmax  43005  ralopabb  43190  clsk3nimkb  43819  ndisj2  44764  eliin2f  44817  infrpge  45077  infxrbnd2  45095  supminfxr  45190  rexanuz2nf  45219  limcrecl  45361  limsupub  45436  limsuppnflem  45442  limsupre2lem  45456  stoweidlem14  45746  stoweidlem34  45766  salexct  46066  meaiuninc3v  46216  vonioo  46414  vonicc  46417  tworepnotupword  46616  copisnmnd  47668  pgrpgt2nabl  47867  islindeps  47958  islininds2  47989  ldepslinc  48014  line2ylem  48261  line2xlem  48263