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

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

Proof of Theorem sbceq1a
StepHypRef Expression
1 sbid 2250 . 2 ([𝑥 / 𝑥]𝜑𝜑)
2 dfsbcq2 3779 . 2 (𝑥 = 𝐴 → ([𝑥 / 𝑥]𝜑[𝐴 / 𝑥]𝜑))
31, 2syl5bbr 286 1 (𝑥 = 𝐴 → (𝜑[𝐴 / 𝑥]𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1530  [wsb 2062  [wsbc 3776
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-sbc 3777
This theorem is referenced by:  sbceq2a  3788  elrabsf  3820  cbvralcsf  3929  vtocl2dOLD  3935  reusngf  4611  rexreusng  4616  reuprg0  4637  rmosn  4654  rabsnifsb  4657  euotd  5400  reuop  6142  wfisg  6181  elfvmptrab1w  6790  elfvmptrab1  6791  ralrnmpt  6858  riotass2  7136  riotass  7137  oprabv  7206  elovmporab  7381  elovmporab1w  7382  elovmporab1  7383  ovmpt3rabdm  7394  elovmpt3rab1  7395  tfindes  7565  sbcopeq1a  7739  mpoxopoveq  7876  findcard2  8747  ac6sfi  8751  indexfi  8821  nn0ind-raph  12071  fzrevral  12982  wrdind  14074  wrd2ind  14075  prmind2  16019  elmptrab  22351  isfildlem  22381  2sqreulem4  25944  gropd  26730  grstructd  26731  rspc2daf  30145  opreu2reuALT  30154  ifeqeqx  30211  wrdt2ind  30541  bnj919  31924  bnj976  31935  bnj1468  32004  bnj110  32016  bnj150  32034  bnj151  32035  bnj607  32074  bnj873  32082  bnj849  32083  bnj1388  32189  setinds  32907  dfon2lem1  32912  tfisg  32939  frpoinsg  32965  frinsg  32971  rdgssun  34528  indexdom  34877  sdclem2  34885  sdclem1  34886  fdc1  34889  riotasv2s  35961  elimhyps  35964  sbccomieg  39255  rexrabdioph  39256  rexfrabdioph  39257  aomclem6  39524  pm13.13a  40604  pm13.13b  40605  pm13.14  40606  tratrb  40735  uzwo4  41180  or2expropbilem2  43134  reuf1odnf  43172  ich2exprop  43465  ichnreuop  43466  ichreuopeq  43467  prproropreud  43503  reupr  43516  reuopreuprim  43520
  Copyright terms: Public domain W3C validator