Theorem rexlimdva 2662

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2205  ∃wrex 2523

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 2527  df-rex 2528

This theorem is referenced by:  rexlimdvaa  2663  rexlimivv  2668  rexlimdvv  2669  ralxfrd  4588  rexxfrd  4589  fvelimab  5738  foco2  5932  elunirn  5945  f1elima  5952  mpoexw  6422  tfrlem5  6558  tfrlemibacc  6570  tfrlemibfn  6572  tfr1onlembacc  6586  tfr1onlembfn  6588  tfrcllembacc  6599  tfrcllembfn  6601  frecabcl  6643  nnaordex  6774  nnawordex  6775  ectocld  6848  phpm  7133  dif1enen  7150  fin0  7155  fin0or  7156  fimax2gtri  7172  fidcenum  7239  suplub2ti  7305  supisoex  7313  enomnilem  7442  finomni  7444  enmkvlem  7465  exmidfodomrlemeldju  7515  exmidfodomrlemreseldju  7516  ltexnqq  7739  ltbtwnnqq  7746  prarloclem4  7829  prarloc2  7835  genprndl  7852  genprndu  7853  prmuloc2  7898  1idprl  7921  1idpru  7922  cauappcvgprlemdisj  7982  cauappcvgprlemladdru  7987  cauappcvgprlemladdrl  7988  caucvgprlemladdrl  8009  recexgt0sr  8104  map2psrprg  8136  suplocsrlem  8139  nntopi  8225  cnegexlem1  8465  cnegexlem2  8466  renegcl  8551  aptap  8942  supinfneg  9948  infsupneg  9949  qmulz  9976  elpq  10002  icc0r  10281  exbtwnzlemstep  10634  rebtwn2zlemstep  10639  ioo0  10646  ico0  10648  ioc0  10649  modqmuladd  10755  addmodlteq  10787  frec2uzrand  10794  frecuzrdgtcl  10801  frecuzrdgfunlem  10808  hashunlem  11196  reuccatpfxs1lem  11466  shftlem  11529  caucvgre  11695  resqrexlemgt0  11734  rexico  11935  negfi  11942  climuni  12007  climshftlemg  12016  climcn1  12022  serf0  12066  summodclem2  12097  zsumdc  12099  fsum2dlemstep  12149  mertenslem2  12251  ntrivcvgap  12263  zproddc  12294  fprod2dlemstep  12337  dvds1lem  12517  odd2np1lem  12587  odd2np1  12588  sqoddm1div8z  12601  ltoddhalfle  12608  halfleoddlt  12609  m1expo  12615  divalglemeunn  12636  divalglemex  12637  divalglemeuneg  12638  flodddiv4  12651  bezoutlemaz  12728  bezoutlembz  12729  dvdssqim  12749  ncoprmgcdne1b  12815  coprmdvds2  12819  divgcdcoprm0  12827  cncongr1  12829  cncongr2  12830  dvdsnprmd  12851  rpexp  12879  pythagtriplem1  12992  pc2dvds  13057  difsqpwdvds  13065  oddprmdvds  13081  prmpwdvds  13082  4sqlem11  13128  imasmnd2  13711  dfgrp3mlem  13857  imasgrp2  13867  issubg4m  13950  imasabl  14093  ringinvnzdiv  14297  imasring  14311  dvdsrcl2  14348  dvdsrmul1  14351  isnzr2  14433  lss1d  14661  lssats2  14692  lspsn  14694  dvdsrzring  14881  znunit  14937  znrrg  14938  tgcl  15059  innei  15158  cnptoprest  15234  lmss  15241  lmtopcnp  15245  txlm  15274  blssps  15422  blss  15423  blssexps  15424  blssex  15425  mopni3  15479  metrest  15501  metcnp3  15506  mulc1cncf  15584  cncfco  15586  elply2  15730  gausslemma2dlem1a  16061  lgsquadlem1  16080  2lgsoddprmlem2  16109  uhgrspansubgrlem  16401  pw1ndom3  16904  subctctexmid  16914