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

Theorem rspcimdv 3197
Description: Restricted specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017.)
Hypotheses
Ref Expression
rspcimdv.1  |-  ( ph  ->  A  e.  B )
rspcimdv.2  |-  ( (
ph  /\  x  =  A )  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
rspcimdv  |-  ( 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 rspcimdv
StepHypRef Expression
1 df-ral 2798 . 2  |-  ( A. x  e.  B  ps  <->  A. x ( x  e.  B  ->  ps )
)
2 rspcimdv.1 . . 3  |-  ( ph  ->  A  e.  B )
3 simpr 461 . . . . . . 7  |-  ( (
ph  /\  x  =  A )  ->  x  =  A )
43eleq1d 2512 . . . . . 6  |-  ( (
ph  /\  x  =  A )  ->  (
x  e.  B  <->  A  e.  B ) )
54biimprd 223 . . . . 5  |-  ( (
ph  /\  x  =  A )  ->  ( A  e.  B  ->  x  e.  B ) )
6 rspcimdv.2 . . . . 5  |-  ( (
ph  /\  x  =  A )  ->  ( ps  ->  ch ) )
75, 6imim12d 74 . . . 4  |-  ( (
ph  /\  x  =  A )  ->  (
( x  e.  B  ->  ps )  ->  ( A  e.  B  ->  ch ) ) )
82, 7spcimdv 3177 . . 3  |-  ( ph  ->  ( A. x ( x  e.  B  ->  ps )  ->  ( A  e.  B  ->  ch ) ) )
92, 8mpid 41 . 2  |-  ( ph  ->  ( A. x ( x  e.  B  ->  ps )  ->  ch )
)
101, 9syl5bi 217 1  |-  ( ph  ->  ( A. x  e.  B  ps  ->  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369   A.wal 1381    = 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:  rspcimedv  3198  rspcdv  3199  wrd2ind  12685  mreexd  15021  mreexexlemd  15023  catcocl  15064  catass  15065  moni  15113  subccocl  15193  funcco  15219  fullfo  15260  fthf1  15265  nati  15303  acsfiindd  15786  chpscmat  19321  sizeusglecusglem1  24462  friendshipgt3  25099  lmxrge0  27912  funressnfv  32167
  Copyright terms: Public domain W3C validator