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

Theorem sbcie 3300
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 3298 . 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 1399    e. wcel 1836   _Vcvv 3047   [.wsbc 3265
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-10 1855  ax-12 1872  ax-13 2016  ax-ext 2370
This theorem depends on definitions:  df-bi 185  df-an 369  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-clab 2378  df-cleq 2384  df-clel 2387  df-v 3049  df-sbc 3266
This theorem is referenced by:  tfinds2  6615  findcard2  7693  ac6sfi  7697  ac6num  8790  fpwwe  8953  nn1suc  10491  wrdind  12632  cjth  12957  fprodser  13777  prmind2  14249  joinlem  15777  meetlem  15791  mrcmndind  16133  isghm  16403  islmod  17648  islindf  18951  fgcl  20483  cfinfil  20498  csdfil  20499  supfil  20500  fin1aufil  20537  quotval  22792  soseq  29535  sdclem2  30437  fdc  30440  fdc1  30441  rabren3dioph  30950  2nn0ind  31082  zindbi  31083  onfrALTlem5  33689  bnj62  34155  bnj610  34186  bnj976  34218  bnj106  34308  bnj125  34312  bnj154  34318  bnj155  34319  bnj526  34328  bnj540  34332  bnj591  34351  bnj609  34357  bnj893  34368  bnj1417  34479  lshpkrlem3  35285  hdmap1fval  37972  hdmapfval  38005
  Copyright terms: Public domain W3C validator