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

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

Proof of Theorem sbceq1a
StepHypRef Expression
1 sbid 2248 . 2 ([𝑥 / 𝑥]𝜑𝜑)
2 dfsbcq2 3774 . 2 (𝑥 = 𝐴 → ([𝑥 / 𝑥]𝜑[𝐴 / 𝑥]𝜑))
31, 2syl5bbr 286 1 (𝑥 = 𝐴 → (𝜑[𝐴 / 𝑥]𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1528  [wsb 2060  [wsbc 3771
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-sbc 3772
This theorem is referenced by:  sbceq2a  3783  elrabsf  3815  cbvralcsf  3924  vtocl2dOLD  3930  reusngf  4606  rexreusng  4611  reuprg0  4632  rmosn  4649  rabsnifsb  4652  euotd  5395  reuop  6138  wfisg  6177  elfvmptrab1w  6787  elfvmptrab1  6788  ralrnmpt  6855  riotass2  7133  riotass  7134  oprabv  7203  elovmporab  7380  elovmporab1w  7381  elovmporab1  7382  ovmpt3rabdm  7393  elovmpt3rab1  7394  tfindes  7565  sbcopeq1a  7739  mpoxopoveq  7876  findcard2  8747  ac6sfi  8751  indexfi  8821  nn0ind-raph  12071  fzrevral  12982  wrdind  14074  wrd2ind  14075  prmind2  16019  elmptrab  22365  isfildlem  22395  2sqreulem4  25958  gropd  26744  grstructd  26745  rspc2daf  30159  opreu2reuALT  30168  ifeqeqx  30225  wrdt2ind  30555  bnj919  31938  bnj976  31949  bnj1468  32018  bnj110  32030  bnj150  32048  bnj151  32049  bnj607  32088  bnj873  32096  bnj849  32097  bnj1388  32203  setinds  32921  dfon2lem1  32926  tfisg  32953  frpoinsg  32979  frinsg  32985  rdgssun  34542  indexdom  34892  sdclem2  34900  sdclem1  34901  fdc1  34904  riotasv2s  35976  elimhyps  35979  sbccomieg  39270  rexrabdioph  39271  rexfrabdioph  39272  aomclem6  39539  pm13.13a  40619  pm13.13b  40620  pm13.14  40621  tratrb  40750  uzwo4  41195  or2expropbilem2  43149  reuf1odnf  43187  ich2exprop  43480  ichnreuop  43481  ichreuopeq  43482  prproropreud  43518  reupr  43531  reuopreuprim  43535
  Copyright terms: Public domain W3C validator