Theorem rexlimdva2 3137

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∃wrex 3054

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 3055

This theorem is referenced by:  r19.29an  3138  r19.29a  3142  otiunsndisj  5483  dffo3  7077  omlimcl  8545  cfflb  10219  cfcof  10234  alephval2  10532  pwcfsdom  10543  recexsr  11067  zdiv  12611  modmuladd  13885  ssnn0fi  13957  2cshwcshw  14798  wrdl3s3  14935  s3iunsndisj  14941  odd2np1  16318  mod2eq1n2dvds  16324  m1expo  16352  dvdsnprmd  16667  ncoprmlnprm  16705  lspsneleq  21032  rngqiprngimfo  21218  pzriprnglem4  21401  psgndif  21518  islinds4  21751  cply1coe0bi  22196  mat1dimcrng  22371  smatvscl  22418  cpmatinvcl  22611  pmatcollpw3fi1lem2  22681  fctop  22898  cctop  22900  neindisj  23011  innei  23019  restcld  23066  isnrm3  23253  dis2ndc  23354  fgcl  23772  ufileu  23813  bcthlem5  25235  iundisj  25456  vitalilem2  25517  dcubic  26763  2lgslem1c  27311  2lgslem3a1  27318  2lgslem3b1  27319  2lgslem3c1  27320  2lgslem3d1  27321  f1otrg  28805  umgrnloop  29042  erclwwlkeqlen  29955  erclwwlktr  29958  erclwwlkneqlen  30004  eleclclwwlkn  30012  umgr3v3e3cycl  30120  cusconngr  30127  eucrctshift  30179  2pthfrgr  30220  grpoinvf  30468  nmosetre  30700  blocnilem  30740  shsel3  31251  normcan  31512  nmfnsetre  31813  superpos  32290  iundisjfi  32726  indf1ofs  32796  dfufd2  33528  constrextdg2lem  33745  constrextdg2  33746  esumcst  34060  eulerpartlemgh  34376  afsval  34669  fmlasuc  35380  satffunlem2lem2  35400  brsegle2  36104  heicant  37656  itg2gt0cn  37676  sdclem1  37744  sstotbnd3  37777  prtlem10  38865  zdivgd  42332  prjspeclsp  42607  dffltz  42629  diophrw  42754  eldioph2b  42758  diophin  42767  rexrabdioph  42789  jm2.26a  42996  jm2.27  43004  oadif1lem  43375  oadif1  43376  naddgeoa  43390  naddwordnexlem4  43397  suplesup  45342  uzub  45434  supminfxr  45467  infrpgernmpt  45468  limsuppnflem  45715  limsupubuz  45718  climinf3  45721  limsupre3lem  45737  limsupre3uzlem  45740  limsupvaluz2  45743  supcnvlimsup  45745  limsupresxr  45771  liminfresxr  45772  limsupgtlem  45782  liminfvalxr  45788  liminfreuzlem  45807  cnrefiisplem  45834  xlimmnfvlem2  45838  xlimpnfvlem2  45842  stoweidlem61  46066  carageniuncllem2  46527  icoresmbl  46548  hspmbllem2  46632  ovnovollem3  46663  smflimlem2  46777  smflimlem4  46779  smfmullem3  46798  smfinflem  46822  smfliminflem  46835  fsupdm  46847  finfdm  46851  otiunsndisjX  47284  m1modmmod  47363  sprsymrelf1lem  47496  fmtnoprmfac2lem1  47571  fmtnofac1  47575  lighneallem2  47611  dfodd6  47642  dfeven4  47643  m1expevenALTV  47652  opoeALTV  47688  opeoALTV  47689  mogoldbb  47790  nnsum4primeseven  47805  grimgrtri  47952  uzlidlring  48227  islindeps2  48476  isldepslvec2  48478  eenglngeehlnmlem1  48730