Theorem rexlimdva2 3171

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3093

This theorem is used by:  r19.29an  3172  r19.29a  3176  otiunsndisj  5508  dffo3  7104  omlimcl  8572  cfflb  10261  cfcof  10276  alephval2  10575  pwcfsdom  10586  recexsr  11110  zdiv  12684  modmuladd  13969  ssnn0fi  14041  2cshwcshw  14888  wrdl3s3  15025  s3iunsndisj  15031  odd2np1  16424  mod2eq1n2dvds  16430  m1expo  16458  dvdsnprmd  16773  ncoprmlnprm  16812  lspsneleq  21276  rngqiprngimfo  21478  pzriprnglem4  21671  psgndif  21789  islinds4  22022  cply1coe0bi  22499  mat1dimcrng  22671  smatvscl  22718  cpmatinvcl  22911  pmatcollpw3fi1lem2  22981  fctop  23198  cctop  23200  neindisj  23311  innei  23319  restcld  23366  isnrm3  23553  dis2ndc  23654  fgcl  24072  ufileu  24113  bcthlem5  25524  iundisj  25744  vitalilem2  25805  dcubic  27048  2lgslem1c  27594  2lgslem3a1  27601  2lgslem3b1  27602  2lgslem3c1  27603  2lgslem3d1  27604  f1otrg  29257  umgrnloop  29495  erclwwlkeqlen  30407  erclwwlktr  30410  erclwwlkneqlen  30456  eleclclwwlkn  30464  umgr3v3e3cycl  30572  cusconngr  30579  eucrctshift  30631  2pthfrgr  30672  grpoinvf  30921  nmosetre  31153  blocnilem  31193  shsel3  31704  normcan  31965  nmfnsetre  32266  superpos  32743  iundisjfi  33178  indf1ofs  33223  dfufd2  33871  constrextdg2lem  34169  constrextdg2  34170  esumcst  34484  eulerpartlemgh  34800  afsval  35093  fmlasuc  35899  satffunlem2lem2  35919  brsegle2  36622  heicant  38347  itg2gt0cn  38367  sdclem1  38435  sstotbnd3  38468  prtlem10  39680  zdivgd  43139  prjspeclsp  43385  dffltz  43407  diophrw  43531  eldioph2b  43535  diophin  43544  rexrabdioph  43562  jm2.26a  43768  jm2.27  43776  oadif1lem  44147  oadif1  44148  naddgeoa  44162  naddwordnexlem4  44169  suplesup  46096  uzub  46186  supminfxr  46219  infrpgernmpt  46220  limsuppnflem  46465  limsupubuz  46468  climinf3  46471  limsupre3lem  46487  limsupre3uzlem  46490  limsupvaluz2  46493  supcnvlimsup  46495  limsupresxr  46521  liminfresxr  46522  limsupgtlem  46532  liminfvalxr  46538  liminfreuzlem  46557  cnrefiisplem  46584  xlimmnfvlem2  46588  xlimpnfvlem2  46592  stoweidlem61  46816  carageniuncllem2  47277  icoresmbl  47298  hspmbllem2  47382  ovnovollem3  47413  smflimlem2  47527  smflimlem4  47529  smfmullem3  47548  smfinflem  47572  smfliminflem  47585  fsupdm  47597  finfdm  47601  otiunsndisjX  48057  m1modmmod  48142  sprsymrelf1lem  48281  fmtnoprmfac2lem1  48359  fmtnofac1  48363  lighneallem2  48399  dfodd6  48443  dfeven4  48444  m1expevenALTV  48453  opoeALTV  48489  opeoALTV  48490  mogoldbb  48591  nnsum4primeseven  48606  grimgrtri  48755  uzlidlring  49041  islindeps2  49304  isldepslvec2  49306  eenglngeehlnmlem1  49558