Theorem rexnal 3101

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

Syntax hints:  ¬ wn 3   ↔ wb 205  ∀wral 3062  ∃wrex 3071

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 398  df-ex 1783  df-ral 3063  df-rex 3072

This theorem is referenced by:  r19.35  3109  r19.35OLD  3110  r19.30  3121  rexnal2  3136  rexnal3  3137  2ralorOLD  3230  raleq  3323  elpwunsn  4687  n0snor2el  4834  uni0b  4937  iundif2  5077  weniso  7348  rexrnmpo  7545  onnseq  8341  cofonr  8670  ixp0  8922  boxcutc  8932  isfinite2  9298  ordtypelem9  9518  ordtypelem10  9519  unbndrank  9834  tcrank  9876  infxpenlem  10005  kmlem3  10144  kmlem7  10148  kmlem8  10149  kmlem13  10154  cfeq0  10248  isf32lem2  10346  isf32lem5  10349  isf34lem4  10369  fin1a2lem7  10398  ac6n  10477  alephval2  10564  pwfseqlem3  10652  inttsk  10766  nqereu  10921  npomex  10988  prlem934  11025  arch  12466  qextlt  13179  qextle  13180  xralrple  13181  xrsupsslem  13283  xrinfmsslem  13284  supxrbnd1  13297  supxrbnd2  13298  supxrbnd  13304  fsuppmapnn0fiubex  13954  hashfun  14394  hashge2el2dif  14438  limsuplt  15420  fprodle  15937  alzdvds  16260  isprm5  16641  ncoprmlnprm  16661  pc2dvds  16809  vdwnn  16928  ramcl  16959  cshwshashlem1  17026  cshwshash  17035  isnsgrp  18611  isnmnd  18626  smndex1n0mnd  18790  lt6abl  19758  simpgnideld  19964  mdetunilem8  22113  fctop  22499  cctop  22501  t0dist  22821  ist0-3  22841  pthaus  23134  txkgen  23148  xkohaus  23149  fbfinnfr  23337  isufil2  23404  hausflim  23477  fclscf  23521  bcth  24838  minveclem3b  24937  pmltpc  24959  volsup  25065  volsup2  25114  itg2seq  25252  itg2cn  25273  tdeglem4  25569  tdeglem4OLD  25570  aaliou3lem9  25855  ftalem7  26573  dchrptlem3  26759  dchrsum2  26761  noseponlem  27157  nolt02o  27188  noetasuplem4  27229  noetainflem4  27233  cofcutr  27401  tglowdim1i  27742  tglowdim2ln  27892  brbtwn2  28153  colinearalg  28158  axlowdimlem6  28195  axlowdimlem14  28203  umgr2edg1  28458  umgr2edgneu  28461  nfrgr2v  29515  4cycl2vnunb  29533  nmounbi  30017  nmobndseqi  30020  minvecolem5  30122  fprodex01  32019  xrnarchi  32318  isarchi2  32319  mxidlirred  32577  ssmxidllem  32578  fedgmullem2  32704  ordtconnlem1  32893  lmdvg  32922  hasheuni  33072  voliune  33216  volfiniune  33217  ballotlemodife  33485  ballotlem4  33486  reprdifc  33628  bnj1542  33857  bnj110  33858  bnj1189  34009  dfrecs2  34911  brub  34915  filnetlem4  35255  unblimceq0  35372  relowlpssretop  36234  nlpineqsn  36278  matunitlindflem1  36473  poimirlem23  36500  poimirlem30  36507  poimirlem32  36509  poimir  36510  mblfinlem1  36514  aks4d1p3  40932  aks4d1p8d2  40939  aks6d1c2p2  40946  dffltz  41373  infdesc  41382  fphpd  41540  fiphp3d  41543  rencldnfilem  41544  pellfundglb  41609  onmaxnelsup  41958  onsupnmax  41963  ralopabb  42148  clsk3nimkb  42777  ndisj2  43724  eliin2f  43779  infrpge  44048  infxrbnd2  44066  supminfxr  44161  rexanuz2nf  44190  limcrecl  44332  limsupub  44407  limsuppnflem  44413  limsupre2lem  44427  stoweidlem14  44717  stoweidlem34  44737  salexct  45037  meaiuninc3v  45187  vonioo  45385  vonicc  45388  tworepnotupword  45587  copisnmnd  46566  zrninitoringc  46923  pgrpgt2nabl  46996  islindeps  47088  islininds2  47119  ldepslinc  47144  line2ylem  47391  line2xlem  47393