Theorem rexlimdva 2614

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2167  ∃wrex 2476

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-i5r 1549

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-ral 2480  df-rex 2481

This theorem is referenced by:  rexlimdvaa  2615  rexlimivv  2620  rexlimdvv  2621  ralxfrd  4498  rexxfrd  4499  fvelimab  5620  foco2  5803  elunirn  5816  f1elima  5823  mpoexw  6280  tfrlem5  6381  tfrlemibacc  6393  tfrlemibfn  6395  tfr1onlembacc  6409  tfr1onlembfn  6411  tfrcllembacc  6422  tfrcllembfn  6424  frecabcl  6466  nnaordex  6595  nnawordex  6596  ectocld  6669  phpm  6935  dif1enen  6950  fin0  6955  fin0or  6956  fimax2gtri  6971  fidcenum  7031  suplub2ti  7076  supisoex  7084  enomnilem  7213  finomni  7215  enmkvlem  7236  exmidfodomrlemeldju  7278  exmidfodomrlemreseldju  7279  ltexnqq  7492  ltbtwnnqq  7499  prarloclem4  7582  prarloc2  7588  genprndl  7605  genprndu  7606  prmuloc2  7651  1idprl  7674  1idpru  7675  cauappcvgprlemdisj  7735  cauappcvgprlemladdru  7740  cauappcvgprlemladdrl  7741  caucvgprlemladdrl  7762  recexgt0sr  7857  map2psrprg  7889  suplocsrlem  7892  nntopi  7978  cnegexlem1  8218  cnegexlem2  8219  renegcl  8304  aptap  8694  supinfneg  9686  infsupneg  9687  qmulz  9714  elpq  9740  icc0r  10018  exbtwnzlemstep  10354  rebtwn2zlemstep  10359  ioo0  10366  ico0  10368  ioc0  10369  modqmuladd  10475  addmodlteq  10507  frec2uzrand  10514  frecuzrdgtcl  10521  frecuzrdgfunlem  10528  hashunlem  10913  shftlem  10998  caucvgre  11163  resqrexlemgt0  11202  rexico  11403  negfi  11410  climuni  11475  climshftlemg  11484  climcn1  11490  serf0  11534  summodclem2  11564  zsumdc  11566  fsum2dlemstep  11616  mertenslem2  11718  ntrivcvgap  11730  zproddc  11761  fprod2dlemstep  11804  dvds1lem  11984  odd2np1lem  12054  odd2np1  12055  sqoddm1div8z  12068  ltoddhalfle  12075  halfleoddlt  12076  m1expo  12082  divalglemeunn  12103  divalglemex  12104  divalglemeuneg  12105  flodddiv4  12118  bezoutlemaz  12195  bezoutlembz  12196  dvdssqim  12216  ncoprmgcdne1b  12282  coprmdvds2  12286  divgcdcoprm0  12294  cncongr1  12296  cncongr2  12297  dvdsnprmd  12318  rpexp  12346  pythagtriplem1  12459  pc2dvds  12524  difsqpwdvds  12532  oddprmdvds  12548  prmpwdvds  12549  4sqlem11  12595  imasmnd2  13154  dfgrp3mlem  13300  imasgrp2  13316  issubg4m  13399  imasabl  13542  ringinvnzdiv  13682  imasring  13696  dvdsrcl2  13731  dvdsrmul1  13734  isnzr2  13816  lss1d  14015  lssats2  14046  lspsn  14048  dvdsrzring  14235  znunit  14291  znrrg  14292  tgcl  14384  innei  14483  cnptoprest  14559  lmss  14566  lmtopcnp  14570  txlm  14599  blssps  14747  blss  14748  blssexps  14749  blssex  14750  mopni3  14804  metrest  14826  metcnp3  14831  mulc1cncf  14909  cncfco  14911  elply2  15055  gausslemma2dlem1a  15383  lgsquadlem1  15402  2lgsoddprmlem2  15431  subctctexmid  15731