Theorem rexnal 3085

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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wral 3048  ∃wrex 3057

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 207  df-an 396  df-ex 1781  df-ral 3049  df-rex 3058

This theorem is referenced by:  r19.35  3091  r19.30  3100  rexnal2  3115  rexnal3  3116  raleq  3290  elpwunsn  4636  n0snor2el  4784  uni0b  4884  iundif2  5024  weniso  7294  rexrnmpo  7492  onnseq  8270  cofonr  8595  ixp0  8861  boxcutc  8871  isfinite2  9189  ordtypelem9  9419  ordtypelem10  9420  unbndrank  9742  tcrank  9784  infxpenlem  9911  kmlem3  10051  kmlem7  10055  kmlem8  10056  kmlem13  10061  cfeq0  10154  isf32lem2  10252  isf32lem5  10255  isf34lem4  10275  fin1a2lem7  10304  ac6n  10383  alephval2  10470  pwfseqlem3  10558  inttsk  10672  nqereu  10827  npomex  10894  prlem934  10931  arch  12385  qextlt  13104  qextle  13105  xralrple  13106  xrsupsslem  13208  xrinfmsslem  13209  supxrbnd1  13222  supxrbnd2  13223  supxrbnd  13229  fsuppmapnn0fiubex  13901  hashfun  14346  hashge2el2dif  14389  limsuplt  15388  fprodle  15905  alzdvds  16233  isprm5  16620  ncoprmlnprm  16641  pc2dvds  16793  vdwnn  16912  ramcl  16943  cshwshashlem1  17009  cshwshash  17018  isnsgrp  18633  isnmnd  18648  smndex1n0mnd  18822  lt6abl  19809  simpgnideld  20015  zrninitoringc  20593  psdmul  22082  mdetunilem8  22535  fctop  22920  cctop  22922  t0dist  23241  ist0-3  23261  pthaus  23554  txkgen  23568  xkohaus  23569  fbfinnfr  23757  isufil2  23824  hausflim  23897  fclscf  23941  bcth  25257  minveclem3b  25356  pmltpc  25379  volsup  25485  volsup2  25534  itg2seq  25671  itg2cn  25692  tdeglem4  25993  aaliou3lem9  26286  ftalem7  27017  dchrptlem3  27205  dchrsum2  27207  noseponlem  27604  nolt02o  27635  noetasuplem4  27676  noetainflem4  27680  cofcutr  27869  tglowdim1i  28480  tglowdim2ln  28630  brbtwn2  28885  colinearalg  28890  axlowdimlem6  28927  axlowdimlem14  28935  umgr2edg1  29191  umgr2edgneu  29194  nfrgr2v  30254  4cycl2vnunb  30272  nmounbi  30758  nmobndseqi  30761  minvecolem5  30863  fprodex01  32813  xrnarchi  33160  isarchi2  33161  ssdifidllem  33428  mxidlirred  33444  ssmxidllem  33445  fedgmullem2  33664  ordtconnlem1  33958  lmdvg  33987  hasheuni  34119  voliune  34263  volfiniune  34264  ballotlemodife  34532  ballotlem4  34533  reprdifc  34661  bnj1542  34890  bnj110  34891  bnj1189  35042  dfrecs2  36015  brub  36019  filnetlem4  36446  unblimceq0  36572  relowlpssretop  37429  nlpineqsn  37473  matunitlindflem1  37676  poimirlem23  37703  poimirlem30  37710  poimirlem32  37712  poimir  37713  mblfinlem1  37717  aks4d1p3  42191  aks4d1p8d2  42198  aks6d1c2p2  42232  aks6d1c5  42252  dffltz  42752  infdesc  42761  fphpd  42933  fiphp3d  42936  rencldnfilem  42937  pellfundglb  43002  onmaxnelsup  43340  onsupnmax  43345  ralopabb  43528  clsk3nimkb  44157  ndisj2  45172  eliin2f  45225  infrpge  45474  infxrbnd2  45491  supminfxr  45586  rexanuz2nf  45614  limcrecl  45753  limsupub  45826  limsuppnflem  45832  limsupre2lem  45846  stoweidlem14  46136  stoweidlem34  46156  salexct  46456  meaiuninc3v  46606  vonioo  46804  vonicc  46807  copisnmnd  48293  pgrpgt2nabl  48490  islindeps  48578  islininds2  48609  ldepslinc  48634  line2ylem  48876  line2xlem  48878  iineq0  48944  nelsubclem  49192  setc1onsubc  49727