Theorem rexlimdva2 3166

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 425	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
3	2	rexlimdv 3162	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  ∃wrex 3087

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3088

This theorem is used by:  r19.29an  3167  r19.29a  3171  otiunsndisj  5493  dffo3  7094  omlimcl  8570  cfflb  10318  cfcof  10333  alephval2  10638  pwcfsdom  10649  recexsr  11173  zdiv  12750  modmuladd  14036  ssnn0fi  14108  2cshwcshw  14956  s3rex  15081  wrdl3s3  15095  s3iunsndisj  15101  odd2np1  16491  mod2eq1n2dvds  16497  m1expo  16525  dvdsnprmd  16845  ncoprmlnprm  16884  lspsneleq  21373  rngqiprngimfo  21577  pzriprnglem4  21770  psgndif  21888  islinds4  22121  cply1coe0bi  22600  mat1dimcrng  22772  smatvscl  22819  cpmatinvcl  23015  pmatcollpw3fi1lem2  23085  fctop  23302  cctop  23304  neindisj  23415  innei  23423  restcld  23470  isnrm3  23657  dis2ndc  23759  fgcl  24177  ufileu  24218  bcthlem5  25629  iundisj  25849  vitalilem2  25910  dcubic  27156  2lgslem1c  27702  2lgslem3a1  27709  2lgslem3b1  27710  2lgslem3c1  27711  2lgslem3d1  27712  f1otrg  29430  umgrnloop  29668  erclwwlkeqlen  30592  erclwwlktr  30595  erclwwlkneqlen  30641  eleclclwwlkn  30649  umgr3v3e3cycl  30767  cusconngr  30774  eucrctshift  30826  2pthfrgr  30867  grpoinvf  31116  nmosetre  31348  blocnilem  31388  shsel3  31899  normcan  32160  nmfnsetre  32461  superpos  32938  iundisjfi  33370  indf1ofs  33415  dfufd2  34064  constrextdg2lem  34362  constrextdg2  34363  esumcst  34677  eulerpartlemgh  34993  afsval  35286  fmlasuc  36120  satffunlem2lem2  36140  brsegle2  36844  heicant  38541  itg2gt0cn  38561  sdclem1  38645  sstotbnd3  38678  prtlem10  39890  zdivgd  43356  prjspeclsp  43602  dffltz  43624  diophrw  43723  eldioph2b  43727  diophin  43736  rexrabdioph  43754  jm2.26a  43960  jm2.27  43968  oadif1lem  44339  oadif1  44340  naddgeoa  44354  naddwordnexlem4  44361  suplesup  46295  uzub  46385  supminfxr  46418  infrpgernmpt  46419  limsuppnflem  46664  limsupubuz  46667  climinf3  46670  limsupre3lem  46686  limsupre3uzlem  46689  limsupvaluz2  46692  supcnvlimsup  46694  limsupresxr  46720  liminfresxr  46721  limsupgtlem  46731  liminfvalxr  46737  liminfreuzlem  46756  cnrefiisplem  46783  xlimmnfvlem2  46787  xlimpnfvlem2  46791  stoweidlem61  47015  carageniuncllem2  47476  icoresmbl  47497  hspmbllem2  47581  ovnovollem3  47612  smflimlem2  47726  smflimlem4  47728  smfmullem3  47747  smfinflem  47771  smfliminflem  47784  fsupdm  47796  finfdm  47800  otiunsndisjX  48293  m1modmmod  48378  sprsymrelf1lem  48517  fmtnoprmfac2lem1  48595  fmtnofac1  48599  lighneallem2  48635  dfodd6  48679  dfeven4  48680  m1expevenALTV  48689  opoeALTV  48725  opeoALTV  48726  mogoldbb  48827  nnsum4primeseven  48842  grimgrtri  48991  uzlidlring  49276  islindeps2  49539  isldepslvec2  49541  eenglngeehlnmlem1  49793