Theorem rexlimdva 2651

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2202  ∃wrex 2512

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 2516  df-rex 2517

This theorem is referenced by:  rexlimdvaa  2652  rexlimivv  2657  rexlimdvv  2658  ralxfrd  4565  rexxfrd  4566  fvelimab  5711  foco2  5904  elunirn  5917  f1elima  5924  mpoexw  6387  tfrlem5  6523  tfrlemibacc  6535  tfrlemibfn  6537  tfr1onlembacc  6551  tfr1onlembfn  6553  tfrcllembacc  6564  tfrcllembfn  6566  frecabcl  6608  nnaordex  6739  nnawordex  6740  ectocld  6813  phpm  7095  dif1enen  7112  fin0  7117  fin0or  7118  fimax2gtri  7134  fidcenum  7198  suplub2ti  7243  supisoex  7251  enomnilem  7380  finomni  7382  enmkvlem  7403  exmidfodomrlemeldju  7453  exmidfodomrlemreseldju  7454  ltexnqq  7671  ltbtwnnqq  7678  prarloclem4  7761  prarloc2  7767  genprndl  7784  genprndu  7785  prmuloc2  7830  1idprl  7853  1idpru  7854  cauappcvgprlemdisj  7914  cauappcvgprlemladdru  7919  cauappcvgprlemladdrl  7920  caucvgprlemladdrl  7941  recexgt0sr  8036  map2psrprg  8068  suplocsrlem  8071  nntopi  8157  cnegexlem1  8397  cnegexlem2  8398  renegcl  8483  aptap  8873  supinfneg  9872  infsupneg  9873  qmulz  9900  elpq  9926  icc0r  10204  exbtwnzlemstep  10551  rebtwn2zlemstep  10556  ioo0  10563  ico0  10565  ioc0  10566  modqmuladd  10672  addmodlteq  10704  frec2uzrand  10711  frecuzrdgtcl  10718  frecuzrdgfunlem  10725  hashunlem  11111  reuccatpfxs1lem  11374  shftlem  11437  caucvgre  11602  resqrexlemgt0  11641  rexico  11842  negfi  11849  climuni  11914  climshftlemg  11923  climcn1  11929  serf0  11973  summodclem2  12004  zsumdc  12006  fsum2dlemstep  12056  mertenslem2  12158  ntrivcvgap  12170  zproddc  12201  fprod2dlemstep  12244  dvds1lem  12424  odd2np1lem  12494  odd2np1  12495  sqoddm1div8z  12508  ltoddhalfle  12515  halfleoddlt  12516  m1expo  12522  divalglemeunn  12543  divalglemex  12544  divalglemeuneg  12545  flodddiv4  12558  bezoutlemaz  12635  bezoutlembz  12636  dvdssqim  12656  ncoprmgcdne1b  12722  coprmdvds2  12726  divgcdcoprm0  12734  cncongr1  12736  cncongr2  12737  dvdsnprmd  12758  rpexp  12786  pythagtriplem1  12899  pc2dvds  12964  difsqpwdvds  12972  oddprmdvds  12988  prmpwdvds  12989  4sqlem11  13035  imasmnd2  13596  dfgrp3mlem  13742  imasgrp2  13758  issubg4m  13841  imasabl  13984  ringinvnzdiv  14125  imasring  14139  dvdsrcl2  14175  dvdsrmul1  14178  isnzr2  14260  lss1d  14459  lssats2  14490  lspsn  14492  dvdsrzring  14679  znunit  14735  znrrg  14736  tgcl  14855  innei  14954  cnptoprest  15030  lmss  15037  lmtopcnp  15041  txlm  15070  blssps  15218  blss  15219  blssexps  15220  blssex  15221  mopni3  15275  metrest  15297  metcnp3  15302  mulc1cncf  15380  cncfco  15382  elply2  15526  gausslemma2dlem1a  15857  lgsquadlem1  15876  2lgsoddprmlem2  15905  uhgrspansubgrlem  16197  pw1ndom3  16690  subctctexmid  16702