ILE Home 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  6438  nn0ind-raph  8353  indstr  8534  fzrevral  8965  bj-intabssel  9902  bj-bdfindes  10048  bj-findes  10080
  Copyright terms: Public domain W3C validator