Theorem rexnal 3115

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

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209  ∀wral 3077  ∃wrex 3087

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-ral 3078  df-rex 3088

This theorem is used by:  r19.35  3121  r19.30  3130  rexnal2  3145  rexnal3  3146  raleq  3317  elpwunsn  4645  n0snor2el  4793  uni0b  4894  iundif2  5032  weniso  7356  rexrnmpo  7552  onnseq  8336  cofonr  8667  ixp0  8943  boxcutc  8953  isfinite2  9274  ordtypelem9  9504  ordtypelem10  9505  unbndrank  9836  tcrank  9882  infxpenlem  10073  kmlem3  10212  kmlem7  10216  kmlem8  10217  kmlem13  10222  cfeq0  10315  isf32lem2  10413  isf32lem5  10416  isf34lem4  10436  fin1a2lem7  10465  ac6n  10544  alephval2  10638  pwfseqlem3  10726  inttsk  10840  nqereu  10995  npomex  11062  prlem934  11099  arch  12584  qextlt  13314  qextle  13315  xralrple  13316  xrsupsslem  13418  xrinfmsslem  13419  supxrbnd1  13432  supxrbnd2  13433  supxrbnd  13439  fsuppmapnn0fiubex  14115  hashfun  14562  hashge2el2dif  14605  limsuplt  15626  fprodle  16143  alzdvds  16470  isprm5  16863  ncoprmlnprm  16884  pc2dvds  17037  vdwnn  17156  ramcl  17187  cshwshashlem1  17253  cshwshash  17262  isnsgrp  18892  isnmnd  18907  smndex1n0mnd  19091  lt6abl  20089  simpgnideld  20295  zrninitoringc  20908  ssdifidllem  21620  psdmul  22467  mdetunilem8  22914  matunitlindflem1  22974  fctop  23302  cctop  23304  t0dist  23623  ist0-3  23643  pthaus  23937  txkgen  23951  xkohaus  23952  fbfinnfr  24140  isufil2  24207  hausflim  24280  fclscf  24324  bcth  25630  minveclem3b  25729  pmltpc  25751  volsup  25857  volsup2  25906  itg2seq  26043  itg2cn  26064  tdeglem4  26358  rnplynfin  26612  plyconz  26613  aaliou3lem9  26659  ftalem7  27388  dchrptlem3  27575  dchrsum2  27577  infdesc  27949  noseponlem  28003  nolt02o  28034  noetasuplem4  28075  noetainflem4  28079  cofcutr  28292  tglowdim1i  28946  tglowdim2ln  29102  brbtwn2  29465  colinearalg  29470  axlowdimlem6  29507  axlowdimlem14  29515  umgr2edg1  29774  umgr2edgneu  29777  nfrgr2v  30855  4cycl2vnunb  30873  nmounbi  31360  nmobndseqi  31363  minvecolem5  31465  fprodex01  33398  xrnarchi  33727  isarchi2  33728  mxidlirred  33979  ssmxidllem  33980  fedgmullem2  34244  ordtconnlem1  34538  lmdvg  34567  hasheuni  34699  voliune  34844  volfiniune  34845  ballotlemodife  35113  ballotlem4  35114  reprdifc  35239  bnj1542  35470  bnj110  35471  bnj1189  35622  noinfepregs  35774  dfrecs2  36684  brub  36688  ltnadd  36937  naddle  36938  filnetlem4  37139  unblimceq0  37343  relowlpssretop  38255  nlpineqsn  38299  poimirlem23  38529  poimirlem30  38536  poimirlem32  38538  poimir  38539  mblfinlem1  38543  aks4d1p3  43096  aks4d1p8d2  43103  aks6d1c2p2  43137  aks6d1c5  43157  dffltz  43624  fphpd  43776  fiphp3d  43779  rencldnfilem  43780  pellfundglb  43845  onmaxnelsup  44183  onsupnmax  44188  ralopabb  44370  clsk3nimkb  44999  ndisj2  46011  eliin2f  46062  infrpge  46307  infxrbnd2  46324  supminfxr  46418  rexanuz2nf  46446  limcrecl  46585  limsupub  46658  limsuppnflem  46664  limsupre2lem  46678  stoweidlem14  46968  stoweidlem34  46988  salexct  47288  meaiuninc3v  47438  vonioo  47636  vonicc  47639  copisnmnd  49210  pgrpgt2nabl  49422  islindeps  49509  islininds2  49540  ldepslinc  49565  line2ylem  49807  line2xlem  49809  iineq0  49874  nelsubclem  50119  setc1onsubc  50654