Theorem rexnal 3081

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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wral 3044  ∃wrex 3053

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-ral 3045  df-rex 3054

This theorem is referenced by:  r19.35  3087  r19.30  3096  rexnal2  3111  rexnal3  3112  raleq  3287  elpwunsn  4638  n0snor2el  4787  uni0b  4887  iundif2  5026  weniso  7295  rexrnmpo  7493  onnseq  8274  cofonr  8599  ixp0  8865  boxcutc  8875  isfinite2  9203  ordtypelem9  9437  ordtypelem10  9438  unbndrank  9757  tcrank  9799  infxpenlem  9926  kmlem3  10066  kmlem7  10070  kmlem8  10071  kmlem13  10076  cfeq0  10169  isf32lem2  10267  isf32lem5  10270  isf34lem4  10290  fin1a2lem7  10319  ac6n  10398  alephval2  10485  pwfseqlem3  10573  inttsk  10687  nqereu  10842  npomex  10909  prlem934  10946  arch  12400  qextlt  13124  qextle  13125  xralrple  13126  xrsupsslem  13228  xrinfmsslem  13229  supxrbnd1  13242  supxrbnd2  13243  supxrbnd  13249  fsuppmapnn0fiubex  13918  hashfun  14363  hashge2el2dif  14406  limsuplt  15405  fprodle  15922  alzdvds  16250  isprm5  16637  ncoprmlnprm  16658  pc2dvds  16810  vdwnn  16929  ramcl  16960  cshwshashlem1  17026  cshwshash  17035  isnsgrp  18616  isnmnd  18631  smndex1n0mnd  18805  lt6abl  19793  simpgnideld  19999  zrninitoringc  20580  psdmul  22070  mdetunilem8  22523  fctop  22908  cctop  22910  t0dist  23229  ist0-3  23249  pthaus  23542  txkgen  23556  xkohaus  23557  fbfinnfr  23745  isufil2  23812  hausflim  23885  fclscf  23929  bcth  25246  minveclem3b  25345  pmltpc  25368  volsup  25474  volsup2  25523  itg2seq  25660  itg2cn  25681  tdeglem4  25982  aaliou3lem9  26275  ftalem7  27006  dchrptlem3  27194  dchrsum2  27196  noseponlem  27593  nolt02o  27624  noetasuplem4  27665  noetainflem4  27669  cofcutr  27856  tglowdim1i  28465  tglowdim2ln  28615  brbtwn2  28869  colinearalg  28874  axlowdimlem6  28911  axlowdimlem14  28919  umgr2edg1  29175  umgr2edgneu  29178  nfrgr2v  30235  4cycl2vnunb  30253  nmounbi  30739  nmobndseqi  30742  minvecolem5  30844  fprodex01  32789  xrnarchi  33145  isarchi2  33146  ssdifidllem  33412  mxidlirred  33428  ssmxidllem  33429  fedgmullem2  33616  ordtconnlem1  33910  lmdvg  33939  hasheuni  34071  voliune  34215  volfiniune  34216  ballotlemodife  34485  ballotlem4  34486  reprdifc  34614  bnj1542  34843  bnj110  34844  bnj1189  34995  dfrecs2  35943  brub  35947  filnetlem4  36374  unblimceq0  36500  relowlpssretop  37357  nlpineqsn  37401  matunitlindflem1  37615  poimirlem23  37642  poimirlem30  37649  poimirlem32  37651  poimir  37652  mblfinlem1  37656  aks4d1p3  42071  aks4d1p8d2  42078  aks6d1c2p2  42112  aks6d1c5  42132  dffltz  42627  infdesc  42636  fphpd  42809  fiphp3d  42812  rencldnfilem  42813  pellfundglb  42878  onmaxnelsup  43216  onsupnmax  43221  ralopabb  43404  clsk3nimkb  44033  ndisj2  45049  eliin2f  45102  infrpge  45351  infxrbnd2  45368  supminfxr  45463  rexanuz2nf  45491  limcrecl  45630  limsupub  45705  limsuppnflem  45711  limsupre2lem  45725  stoweidlem14  46015  stoweidlem34  46035  salexct  46335  meaiuninc3v  46485  vonioo  46683  vonicc  46686  tworepnotupword  46887  copisnmnd  48173  pgrpgt2nabl  48370  islindeps  48458  islininds2  48489  ldepslinc  48514  line2ylem  48756  line2xlem  48758  iineq0  48824  nelsubclem  49072  setc1onsubc  49607