MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rspcdv Structured version   Unicode version

Theorem rspcdv 3199
Description: Restricted specialization, using implicit substitution. (Contributed by NM, 17-Feb-2007.) (Revised by Mario Carneiro, 4-Jan-2017.)
Hypotheses
Ref Expression
rspcdv.1  |-  ( ph  ->  A  e.  B )
rspcdv.2  |-  ( (
ph  /\  x  =  A )  ->  ( ps 
<->  ch ) )
Assertion
Ref Expression
rspcdv  |-  ( ph  ->  ( A. x  e.  B  ps  ->  ch ) )
Distinct variable groups:    x, A    x, B    ph, x    ch, x
Allowed substitution hint:    ps( x)

Proof of Theorem rspcdv
StepHypRef Expression
1 rspcdv.1 . 2  |-  ( ph  ->  A  e.  B )
2 rspcdv.2 . . 3  |-  ( (
ph  /\  x  =  A )  ->  ( ps 
<->  ch ) )
32biimpd 207 . 2  |-  ( (
ph  /\  x  =  A )  ->  ( ps  ->  ch ) )
41, 3rspcimdv 3197 1  |-  ( ph  ->  ( A. x  e.  B  ps  ->  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1383    e. wcel 1804   A.wral 2793
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ral 2798  df-v 3097
This theorem is referenced by:  ralxfrd  4651  suppofss1d  6939  suppofss2d  6940  zindd  10972  wrd2ind  12685  ismri2dad  15016  mreexd  15021  mreexexlemd  15023  catcocl  15064  catass  15065  moni  15113  subccocl  15193  funcco  15219  fullfo  15260  fthf1  15265  nati  15303  mrcmndind  15976  idsrngd  17490  sizeusglecusglem1  24462  fargshiftfva  24617  wlkiswwlk2lem5  24673  usg2wlkeq  24686  clwlkisclwwlklem2a  24763  clwlkisclwwlklem1  24765  clwwisshclww  24785  usg2cwwk2dif  24798  eupatrl  24946  rngurd  27756  esumcvg  28070  orvcelel  28386  signsply0  28486  onint1  29890  ralbinrald  32158  ralxfrd2  32257  snlindsntorlem  32941  rspcdvinvd  37796
  Copyright terms: Public domain W3C validator