Theorem rexnal 3084

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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wral 3047  ∃wrex 3056

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 3048  df-rex 3057

This theorem is referenced by:  r19.35  3090  r19.30  3099  rexnal2  3114  rexnal3  3115  raleq  3289  elpwunsn  4637  n0snor2el  4785  uni0b  4885  iundif2  5022  weniso  7288  rexrnmpo  7486  onnseq  8264  cofonr  8589  ixp0  8855  boxcutc  8865  isfinite2  9182  ordtypelem9  9412  ordtypelem10  9413  unbndrank  9732  tcrank  9774  infxpenlem  9901  kmlem3  10041  kmlem7  10045  kmlem8  10046  kmlem13  10051  cfeq0  10144  isf32lem2  10242  isf32lem5  10245  isf34lem4  10265  fin1a2lem7  10294  ac6n  10373  alephval2  10460  pwfseqlem3  10548  inttsk  10662  nqereu  10817  npomex  10884  prlem934  10921  arch  12375  qextlt  13099  qextle  13100  xralrple  13101  xrsupsslem  13203  xrinfmsslem  13204  supxrbnd1  13217  supxrbnd2  13218  supxrbnd  13224  fsuppmapnn0fiubex  13896  hashfun  14341  hashge2el2dif  14384  limsuplt  15383  fprodle  15900  alzdvds  16228  isprm5  16615  ncoprmlnprm  16636  pc2dvds  16788  vdwnn  16907  ramcl  16938  cshwshashlem1  17004  cshwshash  17013  isnsgrp  18628  isnmnd  18643  smndex1n0mnd  18817  lt6abl  19805  simpgnideld  20011  zrninitoringc  20589  psdmul  22079  mdetunilem8  22532  fctop  22917  cctop  22919  t0dist  23238  ist0-3  23258  pthaus  23551  txkgen  23565  xkohaus  23566  fbfinnfr  23754  isufil2  23821  hausflim  23894  fclscf  23938  bcth  25254  minveclem3b  25353  pmltpc  25376  volsup  25482  volsup2  25531  itg2seq  25668  itg2cn  25689  tdeglem4  25990  aaliou3lem9  26283  ftalem7  27014  dchrptlem3  27202  dchrsum2  27204  noseponlem  27601  nolt02o  27632  noetasuplem4  27673  noetainflem4  27677  cofcutr  27866  tglowdim1i  28477  tglowdim2ln  28627  brbtwn2  28881  colinearalg  28886  axlowdimlem6  28923  axlowdimlem14  28931  umgr2edg1  29187  umgr2edgneu  29190  nfrgr2v  30247  4cycl2vnunb  30265  nmounbi  30751  nmobndseqi  30754  minvecolem5  30856  fprodex01  32803  xrnarchi  33148  isarchi2  33149  ssdifidllem  33416  mxidlirred  33432  ssmxidllem  33433  fedgmullem2  33638  ordtconnlem1  33932  lmdvg  33961  hasheuni  34093  voliune  34237  volfiniune  34238  ballotlemodife  34506  ballotlem4  34507  reprdifc  34635  bnj1542  34864  bnj110  34865  bnj1189  35016  dfrecs2  35983  brub  35987  filnetlem4  36414  unblimceq0  36540  relowlpssretop  37397  nlpineqsn  37441  matunitlindflem1  37655  poimirlem23  37682  poimirlem30  37689  poimirlem32  37691  poimir  37692  mblfinlem1  37696  aks4d1p3  42110  aks4d1p8d2  42117  aks6d1c2p2  42151  aks6d1c5  42171  dffltz  42666  infdesc  42675  fphpd  42848  fiphp3d  42851  rencldnfilem  42852  pellfundglb  42917  onmaxnelsup  43255  onsupnmax  43260  ralopabb  43443  clsk3nimkb  44072  ndisj2  45087  eliin2f  45140  infrpge  45389  infxrbnd2  45406  supminfxr  45501  rexanuz2nf  45529  limcrecl  45668  limsupub  45741  limsuppnflem  45747  limsupre2lem  45761  stoweidlem14  46051  stoweidlem34  46071  salexct  46371  meaiuninc3v  46521  vonioo  46719  vonicc  46722  copisnmnd  48199  pgrpgt2nabl  48396  islindeps  48484  islininds2  48515  ldepslinc  48540  line2ylem  48782  line2xlem  48784  iineq0  48850  nelsubclem  49098  setc1onsubc  49633