Theorem rexlimdva2 3167

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

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

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 3089

This theorem is used by:  r19.29an  3168  r19.29a  3172  otiunsndisj  5501  dffo3  7099  omlimcl  8569  cfflb  10265  cfcof  10280  alephval2  10585  pwcfsdom  10596  recexsr  11120  zdiv  12695  modmuladd  13981  ssnn0fi  14053  2cshwcshw  14900  s3rex  15025  wrdl3s3  15039  s3iunsndisj  15045  odd2np1  16437  mod2eq1n2dvds  16443  m1expo  16471  dvdsnprmd  16786  ncoprmlnprm  16825  lspsneleq  21308  rngqiprngimfo  21510  pzriprnglem4  21703  psgndif  21821  islinds4  22054  cply1coe0bi  22533  mat1dimcrng  22705  smatvscl  22752  cpmatinvcl  22948  pmatcollpw3fi1lem2  23018  fctop  23235  cctop  23237  neindisj  23348  innei  23356  restcld  23403  isnrm3  23590  dis2ndc  23692  fgcl  24110  ufileu  24151  bcthlem5  25562  iundisj  25782  vitalilem2  25843  dcubic  27091  2lgslem1c  27637  2lgslem3a1  27644  2lgslem3b1  27645  2lgslem3c1  27646  2lgslem3d1  27647  f1otrg  29335  umgrnloop  29573  erclwwlkeqlen  30497  erclwwlktr  30500  erclwwlkneqlen  30546  eleclclwwlkn  30554  umgr3v3e3cycl  30672  cusconngr  30679  eucrctshift  30731  2pthfrgr  30772  grpoinvf  31021  nmosetre  31253  blocnilem  31293  shsel3  31804  normcan  32065  nmfnsetre  32366  superpos  32843  iundisjfi  33275  indf1ofs  33320  dfufd2  33968  constrextdg2lem  34266  constrextdg2  34267  esumcst  34581  eulerpartlemgh  34897  afsval  35190  fmlasuc  35973  satffunlem2lem2  35993  brsegle2  36697  heicant  38412  itg2gt0cn  38432  sdclem1  38501  sstotbnd3  38534  prtlem10  39746  zdivgd  43220  prjspeclsp  43466  dffltz  43488  diophrw  43612  eldioph2b  43616  diophin  43625  rexrabdioph  43643  jm2.26a  43849  jm2.27  43857  oadif1lem  44228  oadif1  44229  naddgeoa  44243  naddwordnexlem4  44250  suplesup  46177  uzub  46267  supminfxr  46300  infrpgernmpt  46301  limsuppnflem  46546  limsupubuz  46549  climinf3  46552  limsupre3lem  46568  limsupre3uzlem  46571  limsupvaluz2  46574  supcnvlimsup  46576  limsupresxr  46602  liminfresxr  46603  limsupgtlem  46613  liminfvalxr  46619  liminfreuzlem  46638  cnrefiisplem  46665  xlimmnfvlem2  46669  xlimpnfvlem2  46673  stoweidlem61  46897  carageniuncllem2  47358  icoresmbl  47379  hspmbllem2  47463  ovnovollem3  47494  smflimlem2  47608  smflimlem4  47610  smfmullem3  47629  smfinflem  47653  smfliminflem  47666  fsupdm  47678  finfdm  47682  otiunsndisjX  48175  m1modmmod  48260  sprsymrelf1lem  48399  fmtnoprmfac2lem1  48477  fmtnofac1  48481  lighneallem2  48517  dfodd6  48561  dfeven4  48562  m1expevenALTV  48571  opoeALTV  48607  opeoALTV  48608  mogoldbb  48709  nnsum4primeseven  48724  grimgrtri  48873  uzlidlring  49158  islindeps2  49421  isldepslvec2  49423  eenglngeehlnmlem1  49675