Theorem rexlimdva 2668

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2209  ∃wrex 2529

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-i5r 1588

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533  df-rex 2534

This theorem is referenced by:  rexlimdvaa  2669  rexlimivv  2674  rexlimdvv  2675  ralxfrd  4606  rexxfrd  4607  fvelimab  5756  foco2  5953  elunirn  5966  f1elima  5973  mpoexw  6443  tfrlem5  6579  tfrlemibacc  6591  tfrlemibfn  6593  tfr1onlembacc  6607  tfr1onlembfn  6609  tfrcllembacc  6620  tfrcllembfn  6622  frecabcl  6664  nnaordex  6795  nnawordex  6796  ectocld  6869  phpm  7161  dif1enen  7178  fin0  7183  fin0or  7184  fimax2gtri  7200  fidcenum  7267  suplub2ti  7335  supisoex  7343  enomnilem  7472  finomni  7474  enmkvlem  7495  exmidfodomrlemeldju  7545  exmidfodomrlemreseldju  7546  ltexnqq  7769  ltbtwnnqq  7776  prarloclem4  7859  prarloc2  7865  genprndl  7882  genprndu  7883  prmuloc2  7928  1idprl  7951  1idpru  7952  cauappcvgprlemdisj  8012  cauappcvgprlemladdru  8017  cauappcvgprlemladdrl  8018  caucvgprlemladdrl  8039  recexgt0sr  8134  map2psrprg  8166  suplocsrlem  8169  nntopi  8255  cnegexlem1  8495  cnegexlem2  8496  renegcl  8581  aptap  8972  supinfneg  9978  infsupneg  9979  qmulz  10006  elpq  10032  icc0r  10311  exbtwnzlemstep  10665  rebtwn2zlemstep  10670  ioo0  10677  ico0  10679  ioc0  10680  modqmuladd  10786  addmodlteq  10818  frec2uzrand  10825  frecuzrdgtcl  10832  frecuzrdgfunlem  10839  hashunlem  11227  reuccatpfxs1lem  11501  shftlem  11564  caucvgre  11730  resqrexlemgt0  11769  rexico  11970  negfi  11977  climuni  12042  climshftlemg  12051  climcn1  12057  serf0  12101  summodclem2  12132  zsumdc  12134  fsum2dlemstep  12184  mertenslem2  12286  ntrivcvgap  12298  zproddc  12329  fprod2dlemstep  12372  dvds1lem  12552  odd2np1lem  12622  odd2np1  12623  sqoddm1div8z  12636  ltoddhalfle  12643  halfleoddlt  12644  m1expo  12650  divalglemeunn  12671  divalglemex  12672  divalglemeuneg  12673  flodddiv4  12686  bezoutlemaz  12763  bezoutlembz  12764  dvdssqim  12784  ncoprmgcdne1b  12850  coprmdvds2  12854  divgcdcoprm0  12862  cncongr1  12864  cncongr2  12865  dvdsnprmd  12886  rpexp  12914  pythagtriplem1  13027  pc2dvds  13092  difsqpwdvds  13100  oddprmdvds  13116  prmpwdvds  13117  4sqlem11  13163  imasmnd2  13742  dfgrp3mlem  13886  imasgrp2  13896  issubg4m  13979  imasabl  14123  ringinvnzdiv  14338  imasring  14352  dvdsrcl2  14389  dvdsrmul1  14392  isnzr2  14474  lss1d  14703  lssats2  14734  lspsn  14736  dvdsrzring  14921  znunit  14977  znrrg  14978  tgcl  15148  innei  15247  cnptoprest  15323  lmss  15330  lmtopcnp  15334  txlm  15363  blssps  15511  blss  15512  blssexps  15513  blssex  15514  mopni3  15568  metrest  15590  metcnp3  15595  mulc1cncf  15673  cncfco  15675  elply2  15819  gausslemma2dlem1a  16160  lgsquadlem1  16179  2lgsoddprmlem2  16208  uhgrspansubgrlem  16500  pw1ndom3  17003  subctctexmid  17013