Theorem rexnal 3114

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

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

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

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-ral 3077  df-rex 3087

This theorem is used by:  r19.35  3120  r19.30  3129  rexnal2  3144  rexnal3  3145  raleq  3316  elpwunsn  4641  n0snor2el  4787  uni0b  4893  iundif2  5031  weniso  7365  rexrnmpo  7561  onnseq  8356  cofonr  8687  ixp0  8963  boxcutc  8973  isfinite2  9294  ordtypelem9  9524  ordtypelem10  9525  unbndrank  9859  tcrank  9905  infxpenlem  10096  kmlem3  10235  kmlem7  10239  kmlem8  10240  kmlem13  10245  cfeq0  10338  isf32lem2  10436  isf32lem5  10439  isf34lem4  10459  fin1a2lem7  10488  ac6n  10567  alephval2  10661  pwfseqlem3  10749  inttsk  10863  nqereu  11018  npomex  11085  prlem934  11122  arch  12607  qextlt  13337  qextle  13338  xralrple  13339  xrsupsslem  13441  xrinfmsslem  13442  supxrbnd1  13455  supxrbnd2  13456  supxrbnd  13462  fsuppmapnn0fiubex  14139  hashfun  14586  hashge2el2dif  14629  limsuplt  15652  fprodle  16169  alzdvds  16496  isprm5  16889  ncoprmlnprm  16910  pc2dvds  17063  vdwnn  17182  ramcl  17213  cshwshashlem1  17279  cshwshash  17288  isnsgrp  18918  isnmnd  18933  smndex1n0mnd  19117  lt6abl  20115  simpgnideld  20321  zrninitoringc  20934  ssdifidllem  21646  psdmul  22493  mdetunilem8  22940  matunitlindflem1  23000  fctop  23328  cctop  23330  t0dist  23649  ist0-3  23669  pthaus  23963  txkgen  23977  xkohaus  23978  fbfinnfr  24166  isufil2  24233  hausflim  24306  fclscf  24350  bcth  25656  minveclem3b  25755  pmltpc  25777  volsup  25883  volsup2  25932  itg2seq  26069  itg2cn  26090  tdeglem4  26384  rnplynfin  26636  plyconz  26637  aaliou3lem9  26683  ftalem7  27412  dchrptlem3  27599  dchrsum2  27601  infdesc  27973  noseponlem  28027  nolt02o  28058  noetasuplem4  28099  noetainflem4  28103  cofcutr  28316  tglowdim1i  28970  tglowdim2ln  29126  brbtwn2  29489  colinearalg  29494  axlowdimlem6  29531  axlowdimlem14  29539  umgr2edg1  29798  umgr2edgneu  29801  nfrgr2v  30879  4cycl2vnunb  30897  nmounbi  31384  nmobndseqi  31387  minvecolem5  31489  fprodex01  33463  xrnarchi  33792  isarchi2  33793  mxidlirred  34044  ssmxidllem  34045  fedgmullem2  34309  ordtconnlem1  34603  lmdvg  34632  hasheuni  34764  voliune  34909  volfiniune  34910  ballotlemodife  35177  ballotlem4  35178  reprdifc  35303  bnj1542  35534  bnj110  35535  bnj1189  35686  noinfepregs  35858  dfrecs2  36807  brub  36811  ltnadd  37060  naddle  37061  filnetlem4  37262  unblimceq0  37466  relowlpssretop  38381  nlpineqsn  38425  poimirlem23  38655  poimirlem30  38662  poimirlem32  38664  poimir  38665  mblfinlem1  38669  aks4d1p3  43222  aks4d1p8d2  43229  aks6d1c2p2  43263  aks6d1c5  43283  dffltz  43764  fphpd  43917  fiphp3d  43920  rencldnfilem  43921  pellfundglb  43986  onmaxnelsup  44319  onsupnmax  44324  ralopabb  44506  clsk3nimkb  45134  ndisj2  46162  eliin2f  46213  infrpge  46457  infxrbnd2  46474  supminfxr  46568  rexanuz2nf  46596  limcrecl  46735  limsupub  46808  limsuppnflem  46814  limsupre2lem  46828  stoweidlem14  47118  stoweidlem34  47138  salexct  47438  meaiuninc3v  47588  vonioo  47786  vonicc  47789  copisnmnd  49360  pgrpgt2nabl  49572  islindeps  49659  islininds2  49690  ldepslinc  49715  line2ylem  49957  line2xlem  49959  iineq0  50025  nelsubclem  50275  setc1onsubc  50834