Theorem rexnal 3117

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

Syntax hints:  ¬ wn 3   ↔ wb 209  ∀wral 3079  ∃wrex 3089

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-ral 3080  df-rex 3090

This theorem is referenced by:  r19.35  3123  r19.30  3132  rexnal2  3147  rexnal3  3148  raleq  3320  elpwunsn  4651  n0snor2el  4799  uni0b  4900  iundif2  5039  weniso  7354  rexrnmpo  7552  onnseq  8332  cofonr  8661  ixp0  8930  boxcutc  8940  isfinite2  9259  ordtypelem9  9489  ordtypelem10  9490  unbndrank  9815  tcrank  9857  infxpenlem  9998  kmlem3  10137  kmlem7  10141  kmlem8  10142  kmlem13  10147  cfeq0  10241  isf32lem2  10339  isf32lem5  10342  isf34lem4  10362  fin1a2lem7  10391  ac6n  10470  alephval2  10558  pwfseqlem3  10646  inttsk  10760  nqereu  10915  npomex  10982  prlem934  11019  arch  12502  qextlt  13230  qextle  13231  xralrple  13232  xrsupsslem  13334  xrinfmsslem  13335  supxrbnd1  13348  supxrbnd2  13349  supxrbnd  13355  fsuppmapnn0fiubex  14030  hashfun  14476  hashge2el2dif  14519  limsuplt  15532  fprodle  16052  alzdvds  16379  isprm5  16767  ncoprmlnprm  16788  pc2dvds  16940  vdwnn  17059  ramcl  17090  cshwshashlem1  17156  cshwshash  17165  isnsgrp  18782  isnmnd  18797  smndex1n0mnd  18975  lt6abl  19966  simpgnideld  20172  zrninitoringc  20762  ssdifidllem  21465  psdmul  22310  mdetunilem8  22757  fctop  23142  cctop  23144  t0dist  23463  ist0-3  23483  pthaus  23776  txkgen  23790  xkohaus  23791  fbfinnfr  23979  isufil2  24046  hausflim  24119  fclscf  24163  bcth  25469  minveclem3b  25568  pmltpc  25590  volsup  25696  volsup2  25745  itg2seq  25882  itg2cn  25903  tdeglem4  26198  aaliou3lem9  26494  ftalem7  27224  dchrptlem3  27411  dchrsum2  27413  noseponlem  27809  nolt02o  27840  noetasuplem4  27881  noetainflem4  27885  cofcutr  28098  tglowdim1i  28751  tglowdim2ln  28906  brbtwn2  29236  colinearalg  29241  axlowdimlem6  29278  axlowdimlem14  29286  umgr2edg1  29542  umgr2edgneu  29545  nfrgr2v  30604  4cycl2vnunb  30622  nmounbi  31109  nmobndseqi  31112  minvecolem5  31214  fprodex01  33150  xrnarchi  33485  isarchi2  33486  mxidlirred  33736  ssmxidllem  33737  fedgmullem2  34001  ordtconnlem1  34295  lmdvg  34324  hasheuni  34456  voliune  34600  volfiniune  34601  ballotlemodife  34869  ballotlem4  34870  reprdifc  34995  bnj1542  35226  bnj110  35227  bnj1189  35378  noinfepregs  35527  dfrecs2  36423  brub  36427  ltnadd  36676  naddle  36677  filnetlem4  36873  unblimceq0  37077  relowlpssretop  37991  nlpineqsn  38035  matunitlindflem1  38248  poimirlem23  38275  poimirlem30  38282  poimirlem32  38284  poimir  38285  mblfinlem1  38289  aks4d1p3  42826  aks4d1p8d2  42833  aks6d1c2p2  42867  aks6d1c5  42887  dffltz  43349  infdesc  43358  fphpd  43526  fiphp3d  43529  rencldnfilem  43530  pellfundglb  43595  onmaxnelsup  43933  onsupnmax  43938  ralopabb  44120  clsk3nimkb  44749  ndisj2  45754  eliin2f  45805  infrpge  46050  infxrbnd2  46067  supminfxr  46161  rexanuz2nf  46189  limcrecl  46328  limsupub  46401  limsuppnflem  46407  limsupre2lem  46421  stoweidlem14  46711  stoweidlem34  46731  salexct  47031  meaiuninc3v  47181  vonioo  47379  vonicc  47382  copisnmnd  48917  pgrpgt2nabl  49129  islindeps  49216  islininds2  49247  ldepslinc  49272  line2ylem  49514  line2xlem  49516  iineq0  49581  nelsubclem  49828  setc1onsubc  50363