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 2109  ∃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  ax-5 1910

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

This theorem is referenced by:  r19.29an  3137  r19.29a  3141  otiunsndisj  5480  dffo3  7074  omlimcl  8542  cfflb  10212  cfcof  10227  alephval2  10525  pwcfsdom  10536  recexsr  11060  zdiv  12604  modmuladd  13878  ssnn0fi  13950  2cshwcshw  14791  wrdl3s3  14928  s3iunsndisj  14934  odd2np1  16311  mod2eq1n2dvds  16317  m1expo  16345  dvdsnprmd  16660  ncoprmlnprm  16698  lspsneleq  21025  rngqiprngimfo  21211  pzriprnglem4  21394  psgndif  21511  islinds4  21744  cply1coe0bi  22189  mat1dimcrng  22364  smatvscl  22411  cpmatinvcl  22604  pmatcollpw3fi1lem2  22674  fctop  22891  cctop  22893  neindisj  23004  innei  23012  restcld  23059  isnrm3  23246  dis2ndc  23347  fgcl  23765  ufileu  23806  bcthlem5  25228  iundisj  25449  vitalilem2  25510  dcubic  26756  2lgslem1c  27304  2lgslem3a1  27311  2lgslem3b1  27312  2lgslem3c1  27313  2lgslem3d1  27314  f1otrg  28798  umgrnloop  29035  erclwwlkeqlen  29948  erclwwlktr  29951  erclwwlkneqlen  29997  eleclclwwlkn  30005  umgr3v3e3cycl  30113  cusconngr  30120  eucrctshift  30172  2pthfrgr  30213  grpoinvf  30461  nmosetre  30693  blocnilem  30733  shsel3  31244  normcan  31505  nmfnsetre  31806  superpos  32283  iundisjfi  32719  indf1ofs  32789  dfufd2  33521  constrextdg2lem  33738  constrextdg2  33739  esumcst  34053  eulerpartlemgh  34369  afsval  34662  fmlasuc  35373  satffunlem2lem2  35393  brsegle2  36097  heicant  37649  itg2gt0cn  37669  sdclem1  37737  sstotbnd3  37770  prtlem10  38858  zdivgd  42325  prjspeclsp  42600  dffltz  42622  diophrw  42747  eldioph2b  42751  diophin  42760  rexrabdioph  42782  jm2.26a  42989  jm2.27  42997  oadif1lem  43368  oadif1  43369  naddgeoa  43383  naddwordnexlem4  43390  suplesup  45335  uzub  45427  supminfxr  45460  infrpgernmpt  45461  limsuppnflem  45708  limsupubuz  45711  climinf3  45714  limsupre3lem  45730  limsupre3uzlem  45733  limsupvaluz2  45736  supcnvlimsup  45738  limsupresxr  45764  liminfresxr  45765  limsupgtlem  45775  liminfvalxr  45781  liminfreuzlem  45800  cnrefiisplem  45827  xlimmnfvlem2  45831  xlimpnfvlem2  45835  stoweidlem61  46059  carageniuncllem2  46520  icoresmbl  46541  hspmbllem2  46625  ovnovollem3  46656  smflimlem2  46770  smflimlem4  46772  smfmullem3  46791  smfinflem  46815  smfliminflem  46828  fsupdm  46840  finfdm  46844  otiunsndisjX  47280  m1modmmod  47359  sprsymrelf1lem  47492  fmtnoprmfac2lem1  47567  fmtnofac1  47571  lighneallem2  47607  dfodd6  47638  dfeven4  47639  m1expevenALTV  47648  opoeALTV  47684  opeoALTV  47685  mogoldbb  47786  nnsum4primeseven  47801  grimgrtri  47948  uzlidlring  48223  islindeps2  48472  isldepslvec2  48474  eenglngeehlnmlem1  48726