Theorem rexlimdva2 3157

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

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

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 3071

This theorem is referenced by:  r19.29an  3158  r19.29a  3162  otiunsndisj  5525  dffo3  7122  omlimcl  8616  cfflb  10299  cfcof  10314  alephval2  10612  pwcfsdom  10623  recexsr  11147  zdiv  12688  modmuladd  13954  ssnn0fi  14026  2cshwcshw  14864  wrdl3s3  15001  s3iunsndisj  15007  odd2np1  16378  mod2eq1n2dvds  16384  m1expo  16412  dvdsnprmd  16727  ncoprmlnprm  16765  lspsneleq  21117  rngqiprngimfo  21311  pzriprnglem4  21495  psgndif  21620  islinds4  21855  cply1coe0bi  22306  mat1dimcrng  22483  smatvscl  22530  cpmatinvcl  22723  pmatcollpw3fi1lem2  22793  fctop  23011  cctop  23013  neindisj  23125  innei  23133  restcld  23180  isnrm3  23367  dis2ndc  23468  fgcl  23886  ufileu  23927  bcthlem5  25362  iundisj  25583  vitalilem2  25644  dcubic  26889  2lgslem1c  27437  2lgslem3a1  27444  2lgslem3b1  27445  2lgslem3c1  27446  2lgslem3d1  27447  f1otrg  28879  umgrnloop  29125  erclwwlkeqlen  30038  erclwwlktr  30041  erclwwlkneqlen  30087  eleclclwwlkn  30095  umgr3v3e3cycl  30203  cusconngr  30210  eucrctshift  30262  2pthfrgr  30303  grpoinvf  30551  nmosetre  30783  blocnilem  30823  shsel3  31334  normcan  31595  nmfnsetre  31896  superpos  32373  iundisjfi  32798  indf1ofs  32851  dfufd2  33578  constrextdg2lem  33789  constrextdg2  33790  esumcst  34064  eulerpartlemgh  34380  afsval  34686  fmlasuc  35391  satffunlem2lem2  35411  brsegle2  36110  heicant  37662  itg2gt0cn  37682  sdclem1  37750  sstotbnd3  37783  prtlem10  38866  zdivgd  42372  prjspeclsp  42622  dffltz  42644  diophrw  42770  eldioph2b  42774  diophin  42783  rexrabdioph  42805  jm2.26a  43012  jm2.27  43020  oadif1lem  43392  oadif1  43393  naddgeoa  43407  naddwordnexlem4  43414  suplesup  45350  uzub  45442  supminfxr  45475  infrpgernmpt  45476  limsuppnflem  45725  limsupubuz  45728  climinf3  45731  limsupre3lem  45747  limsupre3uzlem  45750  limsupvaluz2  45753  supcnvlimsup  45755  limsupresxr  45781  liminfresxr  45782  liminflelimsuplem  45790  limsupgtlem  45792  liminfvalxr  45798  liminfreuzlem  45817  cnrefiisplem  45844  xlimmnfvlem2  45848  xlimpnfvlem2  45852  stoweidlem61  46076  carageniuncllem2  46537  icoresmbl  46558  hspmbllem2  46642  ovnovollem3  46673  smflimlem2  46787  smflimlem4  46789  smfmullem3  46808  smfinflem  46832  smfliminflem  46845  fsupdm  46857  finfdm  46861  otiunsndisjX  47291  sprsymrelf1lem  47478  fmtnoprmfac2lem1  47553  fmtnofac1  47557  lighneallem2  47593  dfodd6  47624  dfeven4  47625  m1expevenALTV  47634  opoeALTV  47670  opeoALTV  47671  mogoldbb  47772  nnsum4primeseven  47787  grimgrtri  47916  uzlidlring  48151  islindeps2  48400  isldepslvec2  48402  m1modmmod  48442  eenglngeehlnmlem1  48658