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

Theorem sbcie 3366
Description: Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 4-Sep-2004.)
Hypotheses
Ref Expression
sbcie.1  |-  A  e. 
_V
sbcie.2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
sbcie  |-  ( [. A  /  x ]. ph  <->  ps )
Distinct variable groups:    x, A    ps, x
Allowed substitution hint:    ph( x)

Proof of Theorem sbcie
StepHypRef Expression
1 sbcie.1 . 2  |-  A  e. 
_V
2 sbcie.2 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
32sbcieg 3364 . 2  |-  ( A  e.  _V  ->  ( [. A  /  x ]. ph  <->  ps ) )
41, 3ax-mp 5 1  |-  ( [. A  /  x ]. ph  <->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1379    e. wcel 1767   _Vcvv 3113   [.wsbc 3331
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-v 3115  df-sbc 3332
This theorem is referenced by:  tfinds2  6682  findcard2  7760  ac6sfi  7764  ac6num  8859  fpwwe  9024  nn1suc  10557  wrdind  12665  cjth  12899  prmind2  14087  joinlem  15498  meetlem  15512  mrcmndind  15816  isghm  16072  issrg  16961  islmod  17316  islindf  18642  fgcl  20142  cfinfil  20157  csdfil  20158  supfil  20159  fin1aufil  20196  quotval  22450  fprodser  28686  soseq  28939  sdclem2  29866  fdc  29869  fdc1  29870  rabren3dioph  30381  2nn0ind  30513  zindbi  30514  onfrALTlem5  32412  bnj62  32871  bnj610  32901  bnj976  32933  bnj106  33023  bnj125  33027  bnj154  33033  bnj155  33034  bnj526  33043  bnj540  33047  bnj591  33066  bnj609  33072  bnj893  33083  bnj1417  33194  lshpkrlem3  33927  hdmap1fval  36612  hdmapfval  36645
  Copyright terms: Public domain W3C validator