Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  sbceq1a GIF 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 (𝑥 = 𝐴 → (𝜑[𝐴 / 𝑥]𝜑))

Proof of Theorem sbceq1a
StepHypRef Expression
1 sbid 1698 . 2 ([𝑥 / 𝑥]𝜑𝜑)
2 dfsbcq2 2819 . 2 (𝑥 = 𝐴 → ([𝑥 / 𝑥]𝜑[𝐴 / 𝑥]𝜑))
31, 2syl5bbr 192 1 (𝑥 = 𝐴 → (𝜑[𝐴 / 𝑥]𝜑))
 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  4017  ralrnmpt  5341  rexrnmpt  5342  riotass2  5525  riotass  5526  sbcopeq1a  5844  mpt2xopoveq  5889  findcard2  6423  findcard2s  6424  ac6sfi  6431  indpi  6594  nn0ind-raph  8545  indstr  8762  fzrevral  9198  exfzdc  9326  uzsinds  9518  zsupcllemstep  10485  infssuzex  10489  prmind2  10646  bj-intabssel  10750  bj-bdfindes  10902  bj-findes  10934
 Copyright terms: Public domain W3C validator