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

Theorem rspcimdv 3162
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 2753 . 2  |-  ( A. x  e.  B  ps  <->  A. x ( x  e.  B  ->  ps )
)
2 rspcimdv.1 . . 3  |-  ( ph  ->  A  e.  B )
3 simpr 467 . . . . . . 7  |-  ( (
ph  /\  x  =  A )  ->  x  =  A )
43eleq1d 2523 . . . . . 6  |-  ( (
ph  /\  x  =  A )  ->  (
x  e.  B  <->  A  e.  B ) )
54biimprd 231 . . . . 5  |-  ( (
ph  /\  x  =  A )  ->  ( A  e.  B  ->  x  e.  B ) )
6 rspcimdv.2 . . . . 5  |-  ( (
ph  /\  x  =  A )  ->  ( ps  ->  ch ) )
75, 6imim12d 77 . . . 4  |-  ( (
ph  /\  x  =  A )  ->  (
( x  e.  B  ->  ps )  ->  ( A  e.  B  ->  ch ) ) )
82, 7spcimdv 3142 . . 3  |-  ( ph  ->  ( A. x ( x  e.  B  ->  ps )  ->  ( A  e.  B  ->  ch ) ) )
92, 8mpid 42 . 2  |-  ( ph  ->  ( A. x ( x  e.  B  ->  ps )  ->  ch )
)
101, 9syl5bi 225 1  |-  ( ph  ->  ( A. x  e.  B  ps  ->  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375   A.wal 1452    = wceq 1454    e. wcel 1897   A.wral 2748
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ral 2753  df-v 3058
This theorem is referenced by:  rspcimedv  3163  rspcdv  3164  wrd2ind  12870  mreexd  15596  mreexexlemd  15598  catcocl  15639  catass  15640  moni  15689  subccocl  15798  funcco  15824  fullfo  15865  fthf1  15870  nati  15908  acsfiindd  16471  chpscmat  19914  sizeusglecusglem1  25260  friendshipgt3  25897  lmxrge0  28806  funressnfv  38666
  Copyright terms: Public domain W3C validator