Theorem rexlimdva2 3169

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

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

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 1945

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

This theorem is used by:  r19.29an  3170  r19.29a  3174  otiunsndisj  5498  dffo3  7129  omlimcl  8617  cfflb  10367  cfcof  10382  alephval2  10687  pwcfsdom  10698  recexsr  11222  zdiv  12799  modmuladd  14086  ssnn0fi  14158  2cshwcshw  15007  s3rex  15133  wrdl3s3  15147  s3iunsndisj  15153  odd2np1  16543  mod2eq1n2dvds  16549  m1expo  16577  dvdsnprmd  16897  ncoprmlnprm  16936  lspsneleq  21426  rngqiprngimfo  21630  pzriprnglem4  21823  psgndif  21941  islinds4  22174  cply1coe0bi  22653  mat1dimcrng  22825  smatvscl  22872  cpmatinvcl  23068  pmatcollpw3fi1lem2  23138  fctop  23355  cctop  23357  neindisj  23468  innei  23476  restcld  23523  isnrm3  23710  dis2ndc  23812  fgcl  24230  ufileu  24271  bcthlem5  25682  iundisj  25902  vitalilem2  25963  dcubic  27207  2lgslem1c  27753  2lgslem3a1  27760  2lgslem3b1  27761  2lgslem3c1  27762  2lgslem3d1  27763  f1otrg  29481  umgrnloop  29719  erclwwlkeqlen  30643  erclwwlktr  30646  erclwwlkneqlen  30692  eleclclwwlkn  30700  umgr3v3e3cycl  30818  cusconngr  30825  eucrctshift  30877  2pthfrgr  30918  grpoinvf  31167  nmosetre  31399  blocnilem  31439  shsel3  31950  normcan  32211  nmfnsetre  32512  superpos  32989  iundisjfi  33461  indf1ofs  33506  dfufd2  34166  constrextdg2lem  34463  constrextdg2  34464  esumcst  34778  eulerpartlemgh  35093  afsval  35386  fmlasuc  36331  satffunlem2lem2  36351  brsegle2  37065  heicant  38778  itg2gt0cn  38798  sdclem1  38880  sstotbnd3  38913  prtlem10  40125  zdivgd  43592  prjspeclsp  43844  dffltz  43874  diophrw  43974  eldioph2b  43978  diophin  43987  rexrabdioph  44005  jm2.26a  44211  jm2.27  44219  oadif1lem  44584  oadif1  44585  naddgeoa  44599  naddwordnexlem4  44606  suplesup  46566  uzub  46656  supminfxr  46689  infrpgernmpt  46690  limsuppnflem  46935  limsupubuz  46938  climinf3  46941  limsupre3lem  46957  limsupre3uzlem  46960  limsupvaluz2  46963  supcnvlimsup  46965  limsupresxr  46991  liminfresxr  46992  limsupgtlem  47002  liminfvalxr  47008  liminfreuzlem  47027  cnrefiisplem  47054  xlimmnfvlem2  47058  xlimpnfvlem2  47062  stoweidlem61  47286  carageniuncllem2  47747  icoresmbl  47768  hspmbllem2  47852  ovnovollem3  47883  smflimlem2  47997  smflimlem4  47999  smfmullem3  48018  smfinflem  48042  smfliminflem  48055  fsupdm  48067  finfdm  48071  otiunsndisjX  48564  m1modmmod  48649  sprsymrelf1lem  48788  fmtnoprmfac2lem1  48866  fmtnofac1  48870  lighneallem2  48906  dfodd6  48950  dfeven4  48951  m1expevenALTV  48960  opoeALTV  48996  opeoALTV  48997  mogoldbb  49098  nnsum4primeseven  49113  grimgrtri  49262  uzlidlring  49547  islindeps2  49810  isldepslvec2  49812  eenglngeehlnmlem1  50065