Theorem rexlimdva2 3136

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

Step	Hyp	Ref	Expression
1		rexlimdva2.1	. . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒)
2	1	exp31 419	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
3	2	rexlimdv 3132	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  ∃wrex 3057

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3058

This theorem is referenced by:  r19.29an  3137  r19.29a  3141  otiunsndisj  5463  dffo3  7041  omlimcl  8499  cfflb  10157  cfcof  10172  alephval2  10470  pwcfsdom  10481  recexsr  11005  zdiv  12549  modmuladd  13822  ssnn0fi  13894  2cshwcshw  14734  wrdl3s3  14871  s3iunsndisj  14877  odd2np1  16254  mod2eq1n2dvds  16260  m1expo  16288  dvdsnprmd  16603  ncoprmlnprm  16641  lspsneleq  21054  rngqiprngimfo  21240  pzriprnglem4  21423  psgndif  21541  islinds4  21774  cply1coe0bi  22218  mat1dimcrng  22393  smatvscl  22440  cpmatinvcl  22633  pmatcollpw3fi1lem2  22703  fctop  22920  cctop  22922  neindisj  23033  innei  23041  restcld  23088  isnrm3  23275  dis2ndc  23376  fgcl  23794  ufileu  23835  bcthlem5  25256  iundisj  25477  vitalilem2  25538  dcubic  26784  2lgslem1c  27332  2lgslem3a1  27339  2lgslem3b1  27340  2lgslem3c1  27341  2lgslem3d1  27342  f1otrg  28850  umgrnloop  29088  erclwwlkeqlen  30001  erclwwlktr  30004  erclwwlkneqlen  30050  eleclclwwlkn  30058  umgr3v3e3cycl  30166  cusconngr  30173  eucrctshift  30225  2pthfrgr  30266  grpoinvf  30514  nmosetre  30746  blocnilem  30786  shsel3  31297  normcan  31558  nmfnsetre  31859  superpos  32336  iundisjfi  32783  indf1ofs  32854  dfufd2  33522  constrextdg2lem  33782  constrextdg2  33783  esumcst  34097  eulerpartlemgh  34412  afsval  34705  fmlasuc  35451  satffunlem2lem2  35471  brsegle2  36174  heicant  37716  itg2gt0cn  37736  sdclem1  37804  sstotbnd3  37837  prtlem10  38985  zdivgd  42456  prjspeclsp  42731  dffltz  42753  diophrw  42877  eldioph2b  42881  diophin  42890  rexrabdioph  42912  jm2.26a  43118  jm2.27  43126  oadif1lem  43497  oadif1  43498  naddgeoa  43512  naddwordnexlem4  43519  suplesup  45463  uzub  45554  supminfxr  45587  infrpgernmpt  45588  limsuppnflem  45833  limsupubuz  45836  climinf3  45839  limsupre3lem  45855  limsupre3uzlem  45858  limsupvaluz2  45861  supcnvlimsup  45863  limsupresxr  45889  liminfresxr  45890  limsupgtlem  45900  liminfvalxr  45906  liminfreuzlem  45925  cnrefiisplem  45952  xlimmnfvlem2  45956  xlimpnfvlem2  45960  stoweidlem61  46184  carageniuncllem2  46645  icoresmbl  46666  hspmbllem2  46750  ovnovollem3  46781  smflimlem2  46895  smflimlem4  46897  smfmullem3  46916  smfinflem  46940  smfliminflem  46953  fsupdm  46965  finfdm  46969  otiunsndisjX  47404  m1modmmod  47483  sprsymrelf1lem  47616  fmtnoprmfac2lem1  47691  fmtnofac1  47695  lighneallem2  47731  dfodd6  47762  dfeven4  47763  m1expevenALTV  47772  opoeALTV  47808  opeoALTV  47809  mogoldbb  47910  nnsum4primeseven  47925  grimgrtri  48074  uzlidlring  48360  islindeps2  48609  isldepslvec2  48611  eenglngeehlnmlem1  48863