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

Theorem sbcie 3346
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 3344 . 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 1381    e. wcel 1802   _Vcvv 3093   [.wsbc 3311
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-v 3095  df-sbc 3312
This theorem is referenced by:  tfinds2  6680  findcard2  7759  ac6sfi  7763  ac6num  8859  fpwwe  9024  nn1suc  10560  wrdind  12678  cjth  12912  prmind2  14102  joinlem  15512  meetlem  15526  mrcmndind  15868  isghm  16138  islmod  17387  islindf  18717  fgcl  20249  cfinfil  20264  csdfil  20265  supfil  20266  fin1aufil  20303  quotval  22557  fprodser  29053  soseq  29306  sdclem2  30207  fdc  30210  fdc1  30211  rabren3dioph  30721  2nn0ind  30853  zindbi  30854  onfrALTlem5  33042  bnj62  33501  bnj610  33532  bnj976  33564  bnj106  33654  bnj125  33658  bnj154  33664  bnj155  33665  bnj526  33674  bnj540  33678  bnj591  33697  bnj609  33703  bnj893  33714  bnj1417  33825  lshpkrlem3  34560  hdmap1fval  37247  hdmapfval  37280
  Copyright terms: Public domain W3C validator