Theorem rexlimdva2 3141

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3063

This theorem is referenced by:  r19.29an  3142  r19.29a  3146  otiunsndisj  5468  dffo3  7048  omlimcl  8506  cfflb  10172  cfcof  10187  alephval2  10486  pwcfsdom  10497  recexsr  11021  zdiv  12590  modmuladd  13866  ssnn0fi  13938  2cshwcshw  14778  wrdl3s3  14915  s3iunsndisj  14921  odd2np1  16301  mod2eq1n2dvds  16307  m1expo  16335  dvdsnprmd  16650  ncoprmlnprm  16689  lspsneleq  21105  rngqiprngimfo  21291  pzriprnglem4  21474  psgndif  21592  islinds4  21825  cply1coe0bi  22277  mat1dimcrng  22452  smatvscl  22499  cpmatinvcl  22692  pmatcollpw3fi1lem2  22762  fctop  22979  cctop  22981  neindisj  23092  innei  23100  restcld  23147  isnrm3  23334  dis2ndc  23435  fgcl  23853  ufileu  23894  bcthlem5  25305  iundisj  25525  vitalilem2  25586  dcubic  26823  2lgslem1c  27370  2lgslem3a1  27377  2lgslem3b1  27378  2lgslem3c1  27379  2lgslem3d1  27380  f1otrg  28953  umgrnloop  29191  erclwwlkeqlen  30104  erclwwlktr  30107  erclwwlkneqlen  30153  eleclclwwlkn  30161  umgr3v3e3cycl  30269  cusconngr  30276  eucrctshift  30328  2pthfrgr  30369  grpoinvf  30618  nmosetre  30850  blocnilem  30890  shsel3  31401  normcan  31662  nmfnsetre  31963  superpos  32440  iundisjfi  32884  indf1ofs  32941  dfufd2  33625  constrextdg2lem  33908  constrextdg2  33909  esumcst  34223  eulerpartlemgh  34538  afsval  34831  fmlasuc  35584  satffunlem2lem2  35604  brsegle2  36307  heicant  37990  itg2gt0cn  38010  sdclem1  38078  sstotbnd3  38111  prtlem10  39325  zdivgd  42783  prjspeclsp  43059  dffltz  43081  diophrw  43205  eldioph2b  43209  diophin  43218  rexrabdioph  43240  jm2.26a  43446  jm2.27  43454  oadif1lem  43825  oadif1  43826  naddgeoa  43840  naddwordnexlem4  43847  suplesup  45787  uzub  45877  supminfxr  45910  infrpgernmpt  45911  limsuppnflem  46156  limsupubuz  46159  climinf3  46162  limsupre3lem  46178  limsupre3uzlem  46181  limsupvaluz2  46184  supcnvlimsup  46186  limsupresxr  46212  liminfresxr  46213  limsupgtlem  46223  liminfvalxr  46229  liminfreuzlem  46248  cnrefiisplem  46275  xlimmnfvlem2  46279  xlimpnfvlem2  46283  stoweidlem61  46507  carageniuncllem2  46968  icoresmbl  46989  hspmbllem2  47073  ovnovollem3  47104  smflimlem2  47218  smflimlem4  47220  smfmullem3  47239  smfinflem  47263  smfliminflem  47276  fsupdm  47288  finfdm  47292  otiunsndisjX  47739  m1modmmod  47824  sprsymrelf1lem  47963  fmtnoprmfac2lem1  48041  fmtnofac1  48045  lighneallem2  48081  dfodd6  48125  dfeven4  48126  m1expevenALTV  48135  opoeALTV  48171  opeoALTV  48172  mogoldbb  48273  nnsum4primeseven  48288  grimgrtri  48437  uzlidlring  48723  islindeps2  48971  isldepslvec2  48973  eenglngeehlnmlem1  49225