Theorem rexnal 3238

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

Syntax hints:  ¬ wn 3   ↔ wb 208  ∀wral 3138  ∃wrex 3139

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 3143  df-rex 3144

This theorem is referenced by:  rexnal2  3258  rexnal3  3259  r19.35  3341  2ralor  3369  elpwunsn  4621  n0snor2el  4764  uni0b  4864  iundif2  4996  weniso  7107  rexrnmpo  7290  onnseq  7981  ixp0  8495  boxcutc  8505  isfinite2  8776  ordtypelem9  8990  ordtypelem10  8991  unbndrank  9271  tcrank  9313  infxpenlem  9439  kmlem3  9578  kmlem7  9582  kmlem8  9583  kmlem13  9588  cfeq0  9678  isf32lem2  9776  isf32lem5  9779  isf34lem4  9799  fin1a2lem7  9828  ac6n  9907  alephval2  9994  pwfseqlem3  10082  inttsk  10196  nqereu  10351  npomex  10418  prlem934  10455  arch  11895  qextlt  12597  qextle  12598  xralrple  12599  xrsupsslem  12701  xrinfmsslem  12702  supxrbnd1  12715  supxrbnd2  12716  supxrbnd  12722  fsuppmapnn0fiubex  13361  hashfun  13799  hashge2el2dif  13839  limsuplt  14836  fprodle  15350  alzdvds  15670  isprm5  16051  ncoprmlnprm  16068  pc2dvds  16215  vdwnn  16334  ramcl  16365  cshwshashlem1  16429  cshwshash  16438  isnsgrp  17905  isnmnd  17915  smndex1n0mnd  18077  lt6abl  19015  simpgnideld  19221  mdetunilem8  21228  fctop  21612  cctop  21614  t0dist  21933  ist0-3  21953  pthaus  22246  txkgen  22260  xkohaus  22261  fbfinnfr  22449  isufil2  22516  hausflim  22589  fclscf  22633  bcth  23932  minveclem3b  24031  pmltpc  24051  volsup  24157  volsup2  24206  itg2seq  24343  itg2cn  24364  tdeglem4  24654  aaliou3lem9  24939  ftalem7  25656  dchrptlem3  25842  dchrsum2  25844  tglowdim1i  26287  tglowdim2ln  26437  brbtwn2  26691  colinearalg  26696  axlowdimlem6  26733  axlowdimlem14  26741  umgr2edg1  26993  umgr2edgneu  26996  nfrgr2v  28051  4cycl2vnunb  28069  nmounbi  28553  nmobndseqi  28556  minvecolem5  28658  fprodex01  30541  xrnarchi  30813  isarchi2  30814  ssmxidllem  30978  fedgmullem2  31026  ordtconnlem1  31167  lmdvg  31196  hasheuni  31344  voliune  31488  volfiniune  31489  ballotlemodife  31755  ballotlem4  31756  reprdifc  31898  bnj1542  32129  bnj110  32130  bnj1189  32281  noseponlem  33171  nolt02o  33199  noetalem3  33219  dfrecs2  33411  brub  33415  filnetlem4  33729  unblimceq0  33846  relowlpssretop  34648  nlpineqsn  34692  matunitlindflem1  34903  poimirlem23  34930  poimirlem30  34937  poimirlem32  34939  poimir  34940  mblfinlem1  34944  dffltz  39291  fphpd  39433  fiphp3d  39436  rencldnfilem  39437  pellfundglb  39502  clsk3nimkb  40410  ndisj2  41333  eliin2f  41390  infrpge  41639  infxrbnd2  41657  supminfxr  41760  limcrecl  41930  limsupub  42005  limsuppnflem  42011  limsupre2lem  42025  stoweidlem14  42319  stoweidlem34  42339  salexct  42637  meaiuninc3v  42786  vonioo  42984  vonicc  42987  copisnmnd  44096  zrninitoringc  44362  pgrpgt2nabl  44434  islindeps  44528  islininds2  44559  ldepslinc  44584  line2ylem  44758  line2xlem  44760