Theorem rexlimdva2 3154

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105  ∃wrex 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-rex 3068

This theorem is referenced by:  r19.29an  3155  r19.29a  3159  otiunsndisj  5529  dffo3  7121  omlimcl  8614  cfflb  10296  cfcof  10311  alephval2  10609  pwcfsdom  10620  recexsr  11144  zdiv  12685  modmuladd  13950  ssnn0fi  14022  2cshwcshw  14860  wrdl3s3  14997  s3iunsndisj  15003  odd2np1  16374  mod2eq1n2dvds  16380  m1expo  16408  dvdsnprmd  16723  ncoprmlnprm  16761  lspsneleq  21134  rngqiprngimfo  21328  pzriprnglem4  21512  psgndif  21637  islinds4  21872  cply1coe0bi  22321  mat1dimcrng  22498  smatvscl  22545  cpmatinvcl  22738  pmatcollpw3fi1lem2  22808  fctop  23026  cctop  23028  neindisj  23140  innei  23148  restcld  23195  isnrm3  23382  dis2ndc  23483  fgcl  23901  ufileu  23942  bcthlem5  25375  iundisj  25596  vitalilem2  25657  dcubic  26903  2lgslem1c  27451  2lgslem3a1  27458  2lgslem3b1  27459  2lgslem3c1  27460  2lgslem3d1  27461  f1otrg  28893  umgrnloop  29139  erclwwlkeqlen  30047  erclwwlktr  30050  erclwwlkneqlen  30096  eleclclwwlkn  30104  umgr3v3e3cycl  30212  cusconngr  30219  eucrctshift  30271  2pthfrgr  30312  grpoinvf  30560  nmosetre  30792  blocnilem  30832  shsel3  31343  normcan  31604  nmfnsetre  31905  superpos  32382  iundisjfi  32803  dfufd2  33557  indf1ofs  34006  esumcst  34043  eulerpartlemgh  34359  afsval  34664  fmlasuc  35370  satffunlem2lem2  35390  brsegle2  36090  heicant  37641  itg2gt0cn  37661  sdclem1  37729  sstotbnd3  37762  prtlem10  38846  zdivgd  42350  prjspeclsp  42598  dffltz  42620  diophrw  42746  eldioph2b  42750  diophin  42759  rexrabdioph  42781  jm2.26a  42988  jm2.27  42996  oadif1lem  43368  oadif1  43369  naddgeoa  43383  naddwordnexlem4  43390  suplesup  45288  uzub  45380  supminfxr  45413  infrpgernmpt  45414  limsuppnflem  45665  limsupubuz  45668  climinf3  45671  limsupre3lem  45687  limsupre3uzlem  45690  limsupvaluz2  45693  supcnvlimsup  45695  limsupresxr  45721  liminfresxr  45722  liminflelimsuplem  45730  limsupgtlem  45732  liminfvalxr  45738  liminfreuzlem  45757  cnrefiisplem  45784  xlimmnfvlem2  45788  xlimpnfvlem2  45792  stoweidlem61  46016  carageniuncllem2  46477  icoresmbl  46498  hspmbllem2  46582  ovnovollem3  46613  smflimlem2  46727  smflimlem4  46729  smfmullem3  46748  smfinflem  46772  smfliminflem  46785  fsupdm  46797  finfdm  46801  otiunsndisjX  47228  sprsymrelf1lem  47415  fmtnoprmfac2lem1  47490  fmtnofac1  47494  lighneallem2  47530  dfodd6  47561  dfeven4  47562  m1expevenALTV  47571  opoeALTV  47607  opeoALTV  47608  mogoldbb  47709  nnsum4primeseven  47724  grimgrtri  47851  uzlidlring  48078  islindeps2  48328  isldepslvec2  48330  m1modmmod  48370  eenglngeehlnmlem1  48586