Theorem rexlimdva2 3163

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 3159	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∃wrex 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-rex 3077

This theorem is referenced by:  r19.29an  3164  r19.29a  3168  otiunsndisj  5539  dffo3  7136  omlimcl  8634  cfflb  10328  cfcof  10343  alephval2  10641  pwcfsdom  10652  recexsr  11176  zdiv  12713  modmuladd  13964  ssnn0fi  14036  2cshwcshw  14874  wrdl3s3  15011  s3iunsndisj  15017  odd2np1  16389  mod2eq1n2dvds  16395  m1expo  16423  dvdsnprmd  16737  ncoprmlnprm  16775  lspsneleq  21140  rngqiprngimfo  21334  pzriprnglem4  21518  psgndif  21643  islinds4  21878  cply1coe0bi  22327  mat1dimcrng  22504  smatvscl  22551  cpmatinvcl  22744  pmatcollpw3fi1lem2  22814  fctop  23032  cctop  23034  neindisj  23146  innei  23154  restcld  23201  isnrm3  23388  dis2ndc  23489  fgcl  23907  ufileu  23948  bcthlem5  25381  iundisj  25602  vitalilem2  25663  dcubic  26907  2lgslem1c  27455  2lgslem3a1  27462  2lgslem3b1  27463  2lgslem3c1  27464  2lgslem3d1  27465  f1otrg  28897  umgrnloop  29143  erclwwlkeqlen  30051  erclwwlktr  30054  erclwwlkneqlen  30100  eleclclwwlkn  30108  umgr3v3e3cycl  30216  cusconngr  30223  eucrctshift  30275  2pthfrgr  30316  grpoinvf  30564  nmosetre  30796  blocnilem  30836  shsel3  31347  normcan  31608  nmfnsetre  31909  superpos  32386  iundisjfi  32801  dfufd2  33543  indf1ofs  33990  esumcst  34027  eulerpartlemgh  34343  afsval  34648  fmlasuc  35354  satffunlem2lem2  35374  brsegle2  36073  heicant  37615  itg2gt0cn  37635  sdclem1  37703  sstotbnd3  37736  prtlem10  38821  zdivgd  42324  prjspeclsp  42567  dffltz  42589  diophrw  42715  eldioph2b  42719  diophin  42728  rexrabdioph  42750  jm2.26a  42957  jm2.27  42965  oadif1lem  43341  oadif1  43342  naddgeoa  43356  naddwordnexlem4  43363  suplesup  45254  uzub  45346  supminfxr  45379  infrpgernmpt  45380  limsuppnflem  45631  limsupubuz  45634  climinf3  45637  limsupre3lem  45653  limsupre3uzlem  45656  limsupvaluz2  45659  supcnvlimsup  45661  limsupresxr  45687  liminfresxr  45688  liminflelimsuplem  45696  limsupgtlem  45698  liminfvalxr  45704  liminfreuzlem  45723  cnrefiisplem  45750  xlimmnfvlem2  45754  xlimpnfvlem2  45758  stoweidlem61  45982  carageniuncllem2  46443  icoresmbl  46464  hspmbllem2  46548  ovnovollem3  46579  smflimlem2  46693  smflimlem4  46695  smfmullem3  46714  smfinflem  46738  smfliminflem  46751  fsupdm  46763  finfdm  46767  otiunsndisjX  47194  sprsymrelf1lem  47365  fmtnoprmfac2lem1  47440  fmtnofac1  47444  lighneallem2  47480  dfodd6  47511  dfeven4  47512  m1expevenALTV  47521  opoeALTV  47557  opeoALTV  47558  mogoldbb  47659  nnsum4primeseven  47674  grimgrtri  47798  uzlidlring  47958  islindeps2  48212  isldepslvec2  48214  m1modmmod  48255  eenglngeehlnmlem1  48471