MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexlimdva2 Structured version   Visualization version   GIF version

Theorem rexlimdva2 3292
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by Glauco Siliprandi, 2-Jan-2022.)
Hypothesis
Ref Expression
rexlimdva2.1 (((𝜑𝑥𝐴) ∧ 𝜓) → 𝜒)
Assertion
Ref Expression
rexlimdva2 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Distinct variable groups:   𝜒,𝑥   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem rexlimdva2
StepHypRef Expression
1 rexlimdva2.1 . . 3 (((𝜑𝑥𝐴) ∧ 𝜓) → 𝜒)
21exp31 420 . 2 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
32rexlimdv 3288 1 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wcel 2107  wrex 3144
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-ral 3148  df-rex 3149
This theorem is referenced by:  r19.29an  3293  r19.29a  3294  otiunsndisj  5407  dffo3  6866  omlimcl  8199  cfflb  9675  cfcof  9690  alephval2  9988  pwcfsdom  9999  recexsr  10523  zdiv  12046  modmuladd  13276  ssnn0fi  13348  2cshwcshw  14182  wrdl3s3  14321  s3iunsndisj  14323  odd2np1  15685  mod2eq1n2dvds  15691  m1expo  15721  dvdsnprmd  16029  ncoprmlnprm  16063  lspsneleq  19823  cply1coe0bi  20403  psgndif  20681  islinds4  20914  mat1dimcrng  21021  smatvscl  21068  cpmatinvcl  21260  pmatcollpw3fi1lem2  21330  fctop  21547  cctop  21549  neindisj  21660  innei  21668  restcld  21715  isnrm3  21902  dis2ndc  22003  fgcl  22421  ufileu  22462  bcthlem5  23865  iundisj  24083  vitalilem2  24144  dcubic  25356  2lgslem1c  25902  2lgslem3a1  25909  2lgslem3b1  25910  2lgslem3c1  25911  2lgslem3d1  25912  f1otrg  26590  umgrnloop  26826  erclwwlkeqlen  27730  erclwwlktr  27733  erclwwlkneqlen  27780  eleclclwwlkn  27788  umgr3v3e3cycl  27896  cusconngr  27903  eucrctshift  27955  2pthfrgr  27996  grpoinvf  28242  nmosetre  28474  blocnilem  28514  shsel3  29025  normcan  29286  nmfnsetre  29587  superpos  30064  iundisjfi  30451  indf1ofs  31190  esumcst  31227  eulerpartlemgh  31541  afsval  31847  fmlasuc  32536  satffunlem2lem2  32556  trpredtr  32972  brsegle2  33473  heicant  34813  itg2gt0cn  34833  sdclem1  34905  sstotbnd3  34941  prtlem10  35887  prjspeclsp  39146  dffltz  39155  diophrw  39240  eldioph2b  39244  diophin  39253  rexrabdioph  39275  jm2.26a  39481  jm2.27  39489  suplesup  41491  uzub  41589  supminfxr  41624  infrpgernmpt  41625  limsuppnfdlem  41866  limsuppnflem  41875  limsupubuz  41878  climinf3  41881  limsupre3lem  41897  limsupre3uzlem  41900  limsupvaluz2  41903  supcnvlimsup  41905  limsupresxr  41931  liminfresxr  41932  liminflelimsuplem  41940  limsupgtlem  41942  liminfvalxr  41948  liminfreuzlem  41967  cnrefiisplem  41994  xlimmnfvlem2  41998  xlimpnfvlem2  42002  stoweidlem61  42231  carageniuncllem2  42689  icoresmbl  42710  hspmbllem2  42794  ovnovollem3  42825  smflimlem2  42933  smflimlem4  42935  smfmullem3  42953  smfinflem  42976  smfliminflem  42989  otiunsndisjX  43363  sprsymrelf1lem  43504  fmtnoprmfac2lem1  43579  fmtnofac1  43583  lighneallem2  43622  dfodd6  43653  dfeven4  43654  m1expevenALTV  43663  opoeALTV  43699  opeoALTV  43700  mogoldbb  43801  nnsum4primeseven  43816  uzlidlring  44102  islindeps2  44440  isldepslvec2  44442  m1modmmod  44483  eenglngeehlnmlem1  44626
  Copyright terms: Public domain W3C validator