Theorem rexlimdva 2648

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2200  ∃wrex 2509

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-i5r 1581

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-ral 2513  df-rex 2514

This theorem is referenced by:  rexlimdvaa  2649  rexlimivv  2654  rexlimdvv  2655  ralxfrd  4553  rexxfrd  4554  fvelimab  5692  foco2  5883  elunirn  5896  f1elima  5903  mpoexw  6365  tfrlem5  6466  tfrlemibacc  6478  tfrlemibfn  6480  tfr1onlembacc  6494  tfr1onlembfn  6496  tfrcllembacc  6507  tfrcllembfn  6509  frecabcl  6551  nnaordex  6682  nnawordex  6683  ectocld  6756  phpm  7035  dif1enen  7050  fin0  7055  fin0or  7056  fimax2gtri  7071  fidcenum  7131  suplub2ti  7176  supisoex  7184  enomnilem  7313  finomni  7315  enmkvlem  7336  exmidfodomrlemeldju  7385  exmidfodomrlemreseldju  7386  ltexnqq  7603  ltbtwnnqq  7610  prarloclem4  7693  prarloc2  7699  genprndl  7716  genprndu  7717  prmuloc2  7762  1idprl  7785  1idpru  7786  cauappcvgprlemdisj  7846  cauappcvgprlemladdru  7851  cauappcvgprlemladdrl  7852  caucvgprlemladdrl  7873  recexgt0sr  7968  map2psrprg  8000  suplocsrlem  8003  nntopi  8089  cnegexlem1  8329  cnegexlem2  8330  renegcl  8415  aptap  8805  supinfneg  9798  infsupneg  9799  qmulz  9826  elpq  9852  icc0r  10130  exbtwnzlemstep  10475  rebtwn2zlemstep  10480  ioo0  10487  ico0  10489  ioc0  10490  modqmuladd  10596  addmodlteq  10628  frec2uzrand  10635  frecuzrdgtcl  10642  frecuzrdgfunlem  10649  hashunlem  11034  reuccatpfxs1lem  11286  shftlem  11335  caucvgre  11500  resqrexlemgt0  11539  rexico  11740  negfi  11747  climuni  11812  climshftlemg  11821  climcn1  11827  serf0  11871  summodclem2  11901  zsumdc  11903  fsum2dlemstep  11953  mertenslem2  12055  ntrivcvgap  12067  zproddc  12098  fprod2dlemstep  12141  dvds1lem  12321  odd2np1lem  12391  odd2np1  12392  sqoddm1div8z  12405  ltoddhalfle  12412  halfleoddlt  12413  m1expo  12419  divalglemeunn  12440  divalglemex  12441  divalglemeuneg  12442  flodddiv4  12455  bezoutlemaz  12532  bezoutlembz  12533  dvdssqim  12553  ncoprmgcdne1b  12619  coprmdvds2  12623  divgcdcoprm0  12631  cncongr1  12633  cncongr2  12634  dvdsnprmd  12655  rpexp  12683  pythagtriplem1  12796  pc2dvds  12861  difsqpwdvds  12869  oddprmdvds  12885  prmpwdvds  12886  4sqlem11  12932  imasmnd2  13493  dfgrp3mlem  13639  imasgrp2  13655  issubg4m  13738  imasabl  13881  ringinvnzdiv  14021  imasring  14035  dvdsrcl2  14071  dvdsrmul1  14074  isnzr2  14156  lss1d  14355  lssats2  14386  lspsn  14388  dvdsrzring  14575  znunit  14631  znrrg  14632  tgcl  14746  innei  14845  cnptoprest  14921  lmss  14928  lmtopcnp  14932  txlm  14961  blssps  15109  blss  15110  blssexps  15111  blssex  15112  mopni3  15166  metrest  15188  metcnp3  15193  mulc1cncf  15271  cncfco  15273  elply2  15417  gausslemma2dlem1a  15745  lgsquadlem1  15764  2lgsoddprmlem2  15793  pw1ndom3  16383  subctctexmid  16395