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  4688  n0snor2el  4835  uni0b  4938  iundif2  5078  weniso  7351  rexrnmpo  7548  onnseq  8344  cofonr  8673  ixp0  8925  boxcutc  8935  isfinite2  9301  ordtypelem9  9521  ordtypelem10  9522  unbndrank  9837  tcrank  9879  infxpenlem  10008  kmlem3  10147  kmlem7  10151  kmlem8  10152  kmlem13  10157  cfeq0  10251  isf32lem2  10349  isf32lem5  10352  isf34lem4  10372  fin1a2lem7  10401  ac6n  10480  alephval2  10567  pwfseqlem3  10655  inttsk  10769  nqereu  10924  npomex  10991  prlem934  11028  arch  12469  qextlt  13182  qextle  13183  xralrple  13184  xrsupsslem  13286  xrinfmsslem  13287  supxrbnd1  13300  supxrbnd2  13301  supxrbnd  13307  fsuppmapnn0fiubex  13957  hashfun  14397  hashge2el2dif  14441  limsuplt  15423  fprodle  15940  alzdvds  16263  isprm5  16644  ncoprmlnprm  16664  pc2dvds  16812  vdwnn  16931  ramcl  16962  cshwshashlem1  17029  cshwshash  17038  isnsgrp  18614  isnmnd  18629  smndex1n0mnd  18793  lt6abl  19763  simpgnideld  19969  mdetunilem8  22121  fctop  22507  cctop  22509  t0dist  22829  ist0-3  22849  pthaus  23142  txkgen  23156  xkohaus  23157  fbfinnfr  23345  isufil2  23412  hausflim  23485  fclscf  23529  bcth  24846  minveclem3b  24945  pmltpc  24967  volsup  25073  volsup2  25122  itg2seq  25260  itg2cn  25281  tdeglem4  25577  tdeglem4OLD  25578  aaliou3lem9  25863  ftalem7  26583  dchrptlem3  26769  dchrsum2  26771  noseponlem  27167  nolt02o  27198  noetasuplem4  27239  noetainflem4  27243  cofcutr  27411  tglowdim1i  27752  tglowdim2ln  27902  brbtwn2  28163  colinearalg  28168  axlowdimlem6  28205  axlowdimlem14  28213  umgr2edg1  28468  umgr2edgneu  28471  nfrgr2v  29525  4cycl2vnunb  29543  nmounbi  30029  nmobndseqi  30032  minvecolem5  30134  fprodex01  32031  xrnarchi  32330  isarchi2  32331  mxidlirred  32588  ssmxidllem  32589  fedgmullem2  32715  ordtconnlem1  32904  lmdvg  32933  hasheuni  33083  voliune  33227  volfiniune  33228  ballotlemodife  33496  ballotlem4  33497  reprdifc  33639  bnj1542  33868  bnj110  33869  bnj1189  34020  dfrecs2  34922  brub  34926  filnetlem4  35266  unblimceq0  35383  relowlpssretop  36245  nlpineqsn  36289  matunitlindflem1  36484  poimirlem23  36511  poimirlem30  36518  poimirlem32  36520  poimir  36521  mblfinlem1  36525  aks4d1p3  40943  aks4d1p8d2  40950  aks6d1c2p2  40957  dffltz  41376  infdesc  41385  fphpd  41554  fiphp3d  41557  rencldnfilem  41558  pellfundglb  41623  onmaxnelsup  41972  onsupnmax  41977  ralopabb  42162  clsk3nimkb  42791  ndisj2  43738  eliin2f  43793  infrpge  44061  infxrbnd2  44079  supminfxr  44174  rexanuz2nf  44203  limcrecl  44345  limsupub  44420  limsuppnflem  44426  limsupre2lem  44440  stoweidlem14  44730  stoweidlem34  44750  salexct  45050  meaiuninc3v  45200  vonioo  45398  vonicc  45401  tworepnotupword  45600  copisnmnd  46579  zrninitoringc  46969  pgrpgt2nabl  47042  islindeps  47134  islininds2  47165  ldepslinc  47190  line2ylem  47437  line2xlem  47439