Theorem rexnal 3088

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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wral 3050  ∃wrex 3059

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-ral 3051  df-rex 3060

This theorem is referenced by:  r19.35  3095  r19.35OLD  3096  r19.30  3107  rexnal2  3122  rexnal3  3123  2ralorOLD  3219  raleq  3307  elpwunsn  4666  n0snor2el  4815  uni0b  4915  iundif2  5056  weniso  7357  rexrnmpo  7556  onnseq  8367  cofonr  8695  ixp0  8954  boxcutc  8964  isfinite2  9317  ordtypelem9  9549  ordtypelem10  9550  unbndrank  9865  tcrank  9907  infxpenlem  10036  kmlem3  10176  kmlem7  10180  kmlem8  10181  kmlem13  10186  cfeq0  10279  isf32lem2  10377  isf32lem5  10380  isf34lem4  10400  fin1a2lem7  10429  ac6n  10508  alephval2  10595  pwfseqlem3  10683  inttsk  10797  nqereu  10952  npomex  11019  prlem934  11056  arch  12507  qextlt  13228  qextle  13229  xralrple  13230  xrsupsslem  13332  xrinfmsslem  13333  supxrbnd1  13346  supxrbnd2  13347  supxrbnd  13353  fsuppmapnn0fiubex  14016  hashfun  14459  hashge2el2dif  14502  limsuplt  15498  fprodle  16015  alzdvds  16340  isprm5  16727  ncoprmlnprm  16748  pc2dvds  16900  vdwnn  17019  ramcl  17050  cshwshashlem1  17116  cshwshash  17125  isnsgrp  18710  isnmnd  18725  smndex1n0mnd  18899  lt6abl  19886  simpgnideld  20092  zrninitoringc  20649  psdmul  22137  mdetunilem8  22592  fctop  22977  cctop  22979  t0dist  23298  ist0-3  23318  pthaus  23611  txkgen  23625  xkohaus  23626  fbfinnfr  23814  isufil2  23881  hausflim  23954  fclscf  23998  bcth  25318  minveclem3b  25417  pmltpc  25440  volsup  25546  volsup2  25595  itg2seq  25732  itg2cn  25753  tdeglem4  26054  aaliou3lem9  26347  ftalem7  27077  dchrptlem3  27265  dchrsum2  27267  noseponlem  27664  nolt02o  27695  noetasuplem4  27736  noetainflem4  27740  cofcutr  27913  tglowdim1i  28464  tglowdim2ln  28614  brbtwn2  28869  colinearalg  28874  axlowdimlem6  28911  axlowdimlem14  28919  umgr2edg1  29175  umgr2edgneu  29178  nfrgr2v  30238  4cycl2vnunb  30256  nmounbi  30742  nmobndseqi  30745  minvecolem5  30847  fprodex01  32774  xrnarchi  33137  isarchi2  33138  ssdifidllem  33425  mxidlirred  33441  ssmxidllem  33442  fedgmullem2  33622  ordtconnlem1  33864  lmdvg  33893  hasheuni  34027  voliune  34171  volfiniune  34172  ballotlemodife  34441  ballotlem4  34442  reprdifc  34583  bnj1542  34812  bnj110  34813  bnj1189  34964  dfrecs2  35892  brub  35896  filnetlem4  36323  unblimceq0  36449  relowlpssretop  37306  nlpineqsn  37350  matunitlindflem1  37564  poimirlem23  37591  poimirlem30  37598  poimirlem32  37600  poimir  37601  mblfinlem1  37605  aks4d1p3  42020  aks4d1p8d2  42027  aks6d1c2p2  42061  aks6d1c5  42081  dffltz  42589  infdesc  42598  fphpd  42772  fiphp3d  42775  rencldnfilem  42776  pellfundglb  42841  onmaxnelsup  43180  onsupnmax  43185  ralopabb  43369  clsk3nimkb  43998  ndisj2  45001  eliin2f  45054  infrpge  45307  infxrbnd2  45325  supminfxr  45420  rexanuz2nf  45448  limcrecl  45589  limsupub  45664  limsuppnflem  45670  limsupre2lem  45684  stoweidlem14  45974  stoweidlem34  45994  salexct  46294  meaiuninc3v  46444  vonioo  46642  vonicc  46645  tworepnotupword  46846  copisnmnd  48031  pgrpgt2nabl  48228  islindeps  48316  islininds2  48347  ldepslinc  48372  line2ylem  48618  line2xlem  48620