Theorem rexlimdva 2650

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

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

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-i5r 1583

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-ral 2515  df-rex 2516

This theorem is referenced by:  rexlimdvaa  2651  rexlimivv  2656  rexlimdvv  2657  ralxfrd  4559  rexxfrd  4560  fvelimab  5702  foco2  5894  elunirn  5907  f1elima  5914  mpoexw  6378  tfrlem5  6480  tfrlemibacc  6492  tfrlemibfn  6494  tfr1onlembacc  6508  tfr1onlembfn  6510  tfrcllembacc  6521  tfrcllembfn  6523  frecabcl  6565  nnaordex  6696  nnawordex  6697  ectocld  6770  phpm  7052  dif1enen  7069  fin0  7074  fin0or  7075  fimax2gtri  7091  fidcenum  7155  suplub2ti  7200  supisoex  7208  enomnilem  7337  finomni  7339  enmkvlem  7360  exmidfodomrlemeldju  7410  exmidfodomrlemreseldju  7411  ltexnqq  7628  ltbtwnnqq  7635  prarloclem4  7718  prarloc2  7724  genprndl  7741  genprndu  7742  prmuloc2  7787  1idprl  7810  1idpru  7811  cauappcvgprlemdisj  7871  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  caucvgprlemladdrl  7898  recexgt0sr  7993  map2psrprg  8025  suplocsrlem  8028  nntopi  8114  cnegexlem1  8354  cnegexlem2  8355  renegcl  8440  aptap  8830  supinfneg  9829  infsupneg  9830  qmulz  9857  elpq  9883  icc0r  10161  exbtwnzlemstep  10508  rebtwn2zlemstep  10513  ioo0  10520  ico0  10522  ioc0  10523  modqmuladd  10629  addmodlteq  10661  frec2uzrand  10668  frecuzrdgtcl  10675  frecuzrdgfunlem  10682  hashunlem  11068  reuccatpfxs1lem  11331  shftlem  11381  caucvgre  11546  resqrexlemgt0  11585  rexico  11786  negfi  11793  climuni  11858  climshftlemg  11867  climcn1  11873  serf0  11917  summodclem2  11948  zsumdc  11950  fsum2dlemstep  12000  mertenslem2  12102  ntrivcvgap  12114  zproddc  12145  fprod2dlemstep  12188  dvds1lem  12368  odd2np1lem  12438  odd2np1  12439  sqoddm1div8z  12452  ltoddhalfle  12459  halfleoddlt  12460  m1expo  12466  divalglemeunn  12487  divalglemex  12488  divalglemeuneg  12489  flodddiv4  12502  bezoutlemaz  12579  bezoutlembz  12580  dvdssqim  12600  ncoprmgcdne1b  12666  coprmdvds2  12670  divgcdcoprm0  12678  cncongr1  12680  cncongr2  12681  dvdsnprmd  12702  rpexp  12730  pythagtriplem1  12843  pc2dvds  12908  difsqpwdvds  12916  oddprmdvds  12932  prmpwdvds  12933  4sqlem11  12979  imasmnd2  13540  dfgrp3mlem  13686  imasgrp2  13702  issubg4m  13785  imasabl  13928  ringinvnzdiv  14069  imasring  14083  dvdsrcl2  14119  dvdsrmul1  14122  isnzr2  14204  lss1d  14403  lssats2  14434  lspsn  14436  dvdsrzring  14623  znunit  14679  znrrg  14680  tgcl  14794  innei  14893  cnptoprest  14969  lmss  14976  lmtopcnp  14980  txlm  15009  blssps  15157  blss  15158  blssexps  15159  blssex  15160  mopni3  15214  metrest  15236  metcnp3  15241  mulc1cncf  15319  cncfco  15321  elply2  15465  gausslemma2dlem1a  15793  lgsquadlem1  15812  2lgsoddprmlem2  15841  uhgrspansubgrlem  16133  pw1ndom3  16615  subctctexmid  16627