Theorem rexlimdva2 3165

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-rex 3087

This theorem is used by:  r19.29an  3166  r19.29a  3170  otiunsndisj  5492  dffo3  7103  omlimcl  8590  cfflb  10341  cfcof  10356  alephval2  10661  pwcfsdom  10672  recexsr  11196  zdiv  12773  modmuladd  14060  ssnn0fi  14132  2cshwcshw  14981  s3rex  15107  wrdl3s3  15121  s3iunsndisj  15127  odd2np1  16517  mod2eq1n2dvds  16523  m1expo  16551  dvdsnprmd  16871  ncoprmlnprm  16910  lspsneleq  21399  rngqiprngimfo  21603  pzriprnglem4  21796  psgndif  21914  islinds4  22147  cply1coe0bi  22626  mat1dimcrng  22798  smatvscl  22845  cpmatinvcl  23041  pmatcollpw3fi1lem2  23111  fctop  23328  cctop  23330  neindisj  23441  innei  23449  restcld  23496  isnrm3  23683  dis2ndc  23785  fgcl  24203  ufileu  24244  bcthlem5  25655  iundisj  25875  vitalilem2  25936  dcubic  27180  2lgslem1c  27726  2lgslem3a1  27733  2lgslem3b1  27734  2lgslem3c1  27735  2lgslem3d1  27736  f1otrg  29454  umgrnloop  29692  erclwwlkeqlen  30616  erclwwlktr  30619  erclwwlkneqlen  30665  eleclclwwlkn  30673  umgr3v3e3cycl  30791  cusconngr  30798  eucrctshift  30850  2pthfrgr  30891  grpoinvf  31140  nmosetre  31372  blocnilem  31412  shsel3  31923  normcan  32184  nmfnsetre  32485  superpos  32962  iundisjfi  33435  indf1ofs  33480  dfufd2  34129  constrextdg2lem  34427  constrextdg2  34428  esumcst  34742  eulerpartlemgh  35057  afsval  35350  fmlasuc  36238  satffunlem2lem2  36258  brsegle2  36967  heicant  38667  itg2gt0cn  38687  sdclem1  38771  sstotbnd3  38804  prtlem10  40016  zdivgd  43482  prjspeclsp  43734  dffltz  43764  diophrw  43864  eldioph2b  43868  diophin  43877  rexrabdioph  43895  jm2.26a  44101  jm2.27  44109  oadif1lem  44475  oadif1  44476  naddgeoa  44490  naddwordnexlem4  44497  suplesup  46445  uzub  46535  supminfxr  46568  infrpgernmpt  46569  limsuppnflem  46814  limsupubuz  46817  climinf3  46820  limsupre3lem  46836  limsupre3uzlem  46839  limsupvaluz2  46842  supcnvlimsup  46844  limsupresxr  46870  liminfresxr  46871  limsupgtlem  46881  liminfvalxr  46887  liminfreuzlem  46906  cnrefiisplem  46933  xlimmnfvlem2  46937  xlimpnfvlem2  46941  stoweidlem61  47165  carageniuncllem2  47626  icoresmbl  47647  hspmbllem2  47731  ovnovollem3  47762  smflimlem2  47876  smflimlem4  47878  smfmullem3  47897  smfinflem  47921  smfliminflem  47934  fsupdm  47946  finfdm  47950  otiunsndisjX  48443  m1modmmod  48528  sprsymrelf1lem  48667  fmtnoprmfac2lem1  48745  fmtnofac1  48749  lighneallem2  48785  dfodd6  48829  dfeven4  48830  m1expevenALTV  48839  opoeALTV  48875  opeoALTV  48876  mogoldbb  48977  nnsum4primeseven  48992  grimgrtri  49141  uzlidlring  49426  islindeps2  49689  isldepslvec2  49691  eenglngeehlnmlem1  49944