MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sbceq1a Structured version   Visualization version   GIF version

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

Proof of Theorem sbceq1a
StepHypRef Expression
1 sbid 2100 . 2 ([𝑥 / 𝑥]𝜑𝜑)
2 dfsbcq2 3405 . 2 (𝑥 = 𝐴 → ([𝑥 / 𝑥]𝜑[𝐴 / 𝑥]𝜑))
31, 2syl5bbr 273 1 (𝑥 = 𝐴 → (𝜑[𝐴 / 𝑥]𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195   = wceq 1475  [wsb 1867  [wsbc 3402
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-sbc 3403
This theorem is referenced by:  sbceq2a  3414  elrabsf  3441  cbvralcsf  3531  rabsnifsb  4201  euotd  4900  wfisg  5632  elfvmptrab1  6213  ralrnmpt  6276  riotass2  6537  riotass  6538  oprabv  6601  elovmpt2rab  6778  elovmpt2rab1  6779  ovmpt3rabdm  6790  elovmpt3rab1  6791  tfindes  6954  sbcopeq1a  7111  mpt2xopoveq  7232  findcard2  8085  ac6sfi  8089  indexfi  8157  nn0ind-raph  11353  fzrevral  12294  wrdind  13328  wrd2ind  13329  prmind2  15236  elmptrab  21440  isfildlem  21471  gropd  25708  grstructd  25709  vtocl2d  28699  ifeqeqx  28745  bnj919  30091  bnj976  30102  bnj1468  30170  bnj110  30182  bnj150  30200  bnj151  30201  bnj607  30240  bnj873  30248  bnj849  30249  bnj1388  30355  setinds  30927  dfon2lem1  30932  tfisg  30960  frinsg  30986  indexdom  32699  sdclem2  32708  sdclem1  32709  fdc1  32712  riotasv2s  33262  elimhyps  33265  sbccomieg  36375  rexrabdioph  36376  rexfrabdioph  36377  aomclem6  36647  pm13.13a  37630  pm13.13b  37631  pm13.14  37632  tratrb  37767  uzwo4  38246
  Copyright terms: Public domain W3C validator