Theorem rexnal 3150

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

Syntax hints:  ¬ wn 3   ↔ wb 209  ∀wral 3051  ∃wrex 3052

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

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-ral 3056  df-rex 3057

This theorem is referenced by:  rexnal2  3169  rexnal3  3170  r19.35  3245  2ralor  3271  elpwunsn  4585  n0snor2el  4730  uni0b  4833  iundif2  4968  weniso  7141  rexrnmpo  7327  onnseq  8059  ixp0  8590  boxcutc  8600  isfinite2  8907  ordtypelem9  9120  ordtypelem10  9121  unbndrank  9423  tcrank  9465  infxpenlem  9592  kmlem3  9731  kmlem7  9735  kmlem8  9736  kmlem13  9741  cfeq0  9835  isf32lem2  9933  isf32lem5  9936  isf34lem4  9956  fin1a2lem7  9985  ac6n  10064  alephval2  10151  pwfseqlem3  10239  inttsk  10353  nqereu  10508  npomex  10575  prlem934  10612  arch  12052  qextlt  12758  qextle  12759  xralrple  12760  xrsupsslem  12862  xrinfmsslem  12863  supxrbnd1  12876  supxrbnd2  12877  supxrbnd  12883  fsuppmapnn0fiubex  13530  hashfun  13969  hashge2el2dif  14011  limsuplt  15005  fprodle  15521  alzdvds  15844  isprm5  16227  ncoprmlnprm  16247  pc2dvds  16395  vdwnn  16514  ramcl  16545  cshwshashlem1  16612  cshwshash  16621  isnsgrp  18121  isnmnd  18131  smndex1n0mnd  18293  lt6abl  19234  simpgnideld  19440  mdetunilem8  21470  fctop  21855  cctop  21857  t0dist  22176  ist0-3  22196  pthaus  22489  txkgen  22503  xkohaus  22504  fbfinnfr  22692  isufil2  22759  hausflim  22832  fclscf  22876  bcth  24180  minveclem3b  24279  pmltpc  24301  volsup  24407  volsup2  24456  itg2seq  24594  itg2cn  24615  tdeglem4  24911  tdeglem4OLD  24912  aaliou3lem9  25197  ftalem7  25915  dchrptlem3  26101  dchrsum2  26103  tglowdim1i  26546  tglowdim2ln  26696  brbtwn2  26950  colinearalg  26955  axlowdimlem6  26992  axlowdimlem14  27000  umgr2edg1  27253  umgr2edgneu  27256  nfrgr2v  28309  4cycl2vnunb  28327  nmounbi  28811  nmobndseqi  28814  minvecolem5  28916  fprodex01  30813  xrnarchi  31111  isarchi2  31112  ssmxidllem  31309  fedgmullem2  31379  ordtconnlem1  31542  lmdvg  31571  hasheuni  31719  voliune  31863  volfiniune  31864  ballotlemodife  32130  ballotlem4  32131  reprdifc  32273  bnj1542  32504  bnj110  32505  bnj1189  32656  noseponlem  33553  nolt02o  33584  noetasuplem4  33625  noetainflem4  33629  cofcutr  33778  dfrecs2  33938  brub  33942  filnetlem4  34256  unblimceq0  34373  relowlpssretop  35221  nlpineqsn  35265  matunitlindflem1  35459  poimirlem23  35486  poimirlem30  35493  poimirlem32  35495  poimir  35496  mblfinlem1  35500  dffltz  40115  infdesc  40124  fphpd  40282  fiphp3d  40285  rencldnfilem  40286  pellfundglb  40351  clsk3nimkb  41268  ndisj2  42213  eliin2f  42268  infrpge  42504  infxrbnd2  42522  supminfxr  42620  limcrecl  42788  limsupub  42863  limsuppnflem  42869  limsupre2lem  42883  stoweidlem14  43173  stoweidlem34  43193  salexct  43491  meaiuninc3v  43640  vonioo  43838  vonicc  43841  copisnmnd  44979  zrninitoringc  45245  pgrpgt2nabl  45318  islindeps  45410  islininds2  45441  ldepslinc  45466  line2ylem  45713  line2xlem  45715