Theorem rexlimdva 2660

Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 20-Jan-2007.)

Hypothesis

Ref	Expression
rexlimdva.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))

Assertion

Ref	Expression
rexlimdva	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Distinct variable groups:   𝜑,𝑥   𝜒,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem rexlimdva

Step	Hyp	Ref	Expression
1		rexlimdva.1	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))
2	1	ex 115	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
3	2	rexlimdv 2659	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2203  ∃wrex 2521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-i5r 1584

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2525  df-rex 2526

This theorem is referenced by:  rexlimdvaa  2661  rexlimivv  2666  rexlimdvv  2667  ralxfrd  4582  rexxfrd  4583  fvelimab  5732  foco2  5925  elunirn  5938  f1elima  5945  mpoexw  6408  tfrlem5  6544  tfrlemibacc  6556  tfrlemibfn  6558  tfr1onlembacc  6572  tfr1onlembfn  6574  tfrcllembacc  6585  tfrcllembfn  6587  frecabcl  6629  nnaordex  6760  nnawordex  6761  ectocld  6834  phpm  7119  dif1enen  7136  fin0  7141  fin0or  7142  fimax2gtri  7158  fidcenum  7225  suplub2ti  7291  supisoex  7299  enomnilem  7428  finomni  7430  enmkvlem  7451  exmidfodomrlemeldju  7501  exmidfodomrlemreseldju  7502  ltexnqq  7722  ltbtwnnqq  7729  prarloclem4  7812  prarloc2  7818  genprndl  7835  genprndu  7836  prmuloc2  7881  1idprl  7904  1idpru  7905  cauappcvgprlemdisj  7965  cauappcvgprlemladdru  7970  cauappcvgprlemladdrl  7971  caucvgprlemladdrl  7992  recexgt0sr  8087  map2psrprg  8119  suplocsrlem  8122  nntopi  8208  cnegexlem1  8447  cnegexlem2  8448  renegcl  8533  aptap  8923  supinfneg  9926  infsupneg  9927  qmulz  9954  elpq  9980  icc0r  10258  exbtwnzlemstep  10606  rebtwn2zlemstep  10611  ioo0  10618  ico0  10620  ioc0  10621  modqmuladd  10727  addmodlteq  10759  frec2uzrand  10766  frecuzrdgtcl  10773  frecuzrdgfunlem  10780  hashunlem  11166  reuccatpfxs1lem  11434  shftlem  11497  caucvgre  11662  resqrexlemgt0  11701  rexico  11902  negfi  11909  climuni  11974  climshftlemg  11983  climcn1  11989  serf0  12033  summodclem2  12064  zsumdc  12066  fsum2dlemstep  12116  mertenslem2  12218  ntrivcvgap  12230  zproddc  12261  fprod2dlemstep  12304  dvds1lem  12484  odd2np1lem  12554  odd2np1  12555  sqoddm1div8z  12568  ltoddhalfle  12575  halfleoddlt  12576  m1expo  12582  divalglemeunn  12603  divalglemex  12604  divalglemeuneg  12605  flodddiv4  12618  bezoutlemaz  12695  bezoutlembz  12696  dvdssqim  12716  ncoprmgcdne1b  12782  coprmdvds2  12786  divgcdcoprm0  12794  cncongr1  12796  cncongr2  12797  dvdsnprmd  12818  rpexp  12846  pythagtriplem1  12959  pc2dvds  13024  difsqpwdvds  13032  oddprmdvds  13048  prmpwdvds  13049  4sqlem11  13095  imasmnd2  13657  dfgrp3mlem  13803  imasgrp2  13819  issubg4m  13902  imasabl  14045  ringinvnzdiv  14186  imasring  14200  dvdsrcl2  14236  dvdsrmul1  14239  isnzr2  14321  lss1d  14523  lssats2  14554  lspsn  14556  dvdsrzring  14743  znunit  14799  znrrg  14800  tgcl  14921  innei  15020  cnptoprest  15096  lmss  15103  lmtopcnp  15107  txlm  15136  blssps  15284  blss  15285  blssexps  15286  blssex  15287  mopni3  15341  metrest  15363  metcnp3  15368  mulc1cncf  15446  cncfco  15448  elply2  15592  gausslemma2dlem1a  15923  lgsquadlem1  15942  2lgsoddprmlem2  15971  uhgrspansubgrlem  16263  pw1ndom3  16756  subctctexmid  16766