Theorem rexlimdva2 3140

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

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

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 3062

This theorem is referenced by:  r19.29an  3141  r19.29a  3145  otiunsndisj  5474  dffo3  7054  omlimcl  8513  cfflb  10181  cfcof  10196  alephval2  10495  pwcfsdom  10506  recexsr  11030  zdiv  12599  modmuladd  13875  ssnn0fi  13947  2cshwcshw  14787  wrdl3s3  14924  s3iunsndisj  14930  odd2np1  16310  mod2eq1n2dvds  16316  m1expo  16344  dvdsnprmd  16659  ncoprmlnprm  16698  lspsneleq  21113  rngqiprngimfo  21299  pzriprnglem4  21464  psgndif  21582  islinds4  21815  cply1coe0bi  22267  mat1dimcrng  22442  smatvscl  22489  cpmatinvcl  22682  pmatcollpw3fi1lem2  22752  fctop  22969  cctop  22971  neindisj  23082  innei  23090  restcld  23137  isnrm3  23324  dis2ndc  23425  fgcl  23843  ufileu  23884  bcthlem5  25295  iundisj  25515  vitalilem2  25576  dcubic  26810  2lgslem1c  27356  2lgslem3a1  27363  2lgslem3b1  27364  2lgslem3c1  27365  2lgslem3d1  27366  f1otrg  28939  umgrnloop  29177  erclwwlkeqlen  30089  erclwwlktr  30092  erclwwlkneqlen  30138  eleclclwwlkn  30146  umgr3v3e3cycl  30254  cusconngr  30261  eucrctshift  30313  2pthfrgr  30354  grpoinvf  30603  nmosetre  30835  blocnilem  30875  shsel3  31386  normcan  31647  nmfnsetre  31948  superpos  32425  iundisjfi  32869  indf1ofs  32926  dfufd2  33610  constrextdg2lem  33892  constrextdg2  33893  esumcst  34207  eulerpartlemgh  34522  afsval  34815  fmlasuc  35568  satffunlem2lem2  35588  brsegle2  36291  heicant  37976  itg2gt0cn  37996  sdclem1  38064  sstotbnd3  38097  prtlem10  39311  zdivgd  42769  prjspeclsp  43045  dffltz  43067  diophrw  43191  eldioph2b  43195  diophin  43204  rexrabdioph  43222  jm2.26a  43428  jm2.27  43436  oadif1lem  43807  oadif1  43808  naddgeoa  43822  naddwordnexlem4  43829  suplesup  45769  uzub  45859  supminfxr  45892  infrpgernmpt  45893  limsuppnflem  46138  limsupubuz  46141  climinf3  46144  limsupre3lem  46160  limsupre3uzlem  46163  limsupvaluz2  46166  supcnvlimsup  46168  limsupresxr  46194  liminfresxr  46195  limsupgtlem  46205  liminfvalxr  46211  liminfreuzlem  46230  cnrefiisplem  46257  xlimmnfvlem2  46261  xlimpnfvlem2  46265  stoweidlem61  46489  carageniuncllem2  46950  icoresmbl  46971  hspmbllem2  47055  ovnovollem3  47086  smflimlem2  47200  smflimlem4  47202  smfmullem3  47221  smfinflem  47245  smfliminflem  47258  fsupdm  47270  finfdm  47274  otiunsndisjX  47727  m1modmmod  47812  sprsymrelf1lem  47951  fmtnoprmfac2lem1  48029  fmtnofac1  48033  lighneallem2  48069  dfodd6  48113  dfeven4  48114  m1expevenALTV  48123  opoeALTV  48159  opeoALTV  48160  mogoldbb  48261  nnsum4primeseven  48276  grimgrtri  48425  uzlidlring  48711  islindeps2  48959  isldepslvec2  48961  eenglngeehlnmlem1  49213