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

Theorem sbceq1a 2773
 Description: Equality theorem for class substitution. Class version of sbequ12 1654. (Contributed by NM, 26-Sep-2003.)
Assertion
Ref Expression
sbceq1a (𝑥 = 𝐴 → (𝜑[𝐴 / 𝑥]𝜑))

Proof of Theorem sbceq1a
StepHypRef Expression
1 sbid 1657 . 2 ([𝑥 / 𝑥]𝜑𝜑)
2 dfsbcq2 2767 . 2 (𝑥 = 𝐴 → ([𝑥 / 𝑥]𝜑[𝐴 / 𝑥]𝜑))
31, 2syl5bbr 183 1 (𝑥 = 𝐴 → (𝜑[𝐴 / 𝑥]𝜑))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 98   = wceq 1243  [wsb 1645  [wsbc 2764 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-ext 2022 This theorem depends on definitions:  df-bi 110  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-sbc 2765 This theorem is referenced by:  sbceq2a  2774  elrabsf  2801  cbvralcsf  2908  cbvrexcsf  2909  euotd  3991  ralrnmpt  5309  rexrnmpt  5310  riotass2  5494  riotass  5495  sbcopeq1a  5813  mpt2xopoveq  5855  findcard2  6346  findcard2s  6347  ac6sfi  6352  indpi  6440  nn0ind-raph  8355  indstr  8536  fzrevral  8967  bj-intabssel  9928  bj-bdfindes  10074  bj-findes  10106
 Copyright terms: Public domain W3C validator