ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sbceq1a Unicode version

Theorem sbceq1a 2825
Description: Equality theorem for class substitution. Class version of sbequ12 1695. (Contributed by NM, 26-Sep-2003.)
Assertion
Ref Expression
sbceq1a  |-  ( x  =  A  ->  ( ph 
<-> 
[. A  /  x ]. ph ) )

Proof of Theorem sbceq1a
StepHypRef Expression
1 sbid 1698 . 2  |-  ( [ x  /  x ] ph 
<-> 
ph )
2 dfsbcq2 2819 . 2  |-  ( x  =  A  ->  ( [ x  /  x ] ph  <->  [. A  /  x ]. ph ) )
31, 2syl5bbr 192 1  |-  ( x  =  A  ->  ( ph 
<-> 
[. A  /  x ]. ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103    = wceq 1285   [wsb 1686   [.wsbc 2816
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-sbc 2817
This theorem is referenced by:  sbceq2a  2826  elrabsf  2853  cbvralcsf  2965  cbvrexcsf  2966  euotd  4011  ralrnmpt  5335  rexrnmpt  5336  riotass2  5519  riotass  5520  sbcopeq1a  5838  mpt2xopoveq  5883  findcard2  6413  findcard2s  6414  ac6sfi  6421  indpi  6583  nn0ind-raph  8534  indstr  8751  fzrevral  9187  exfzdc  9315  uzsinds  9507  zsupcllemstep  10474  infssuzex  10478  prmind2  10635  bj-intabssel  10735  bj-bdfindes  10887  bj-findes  10919
  Copyright terms: Public domain W3C validator