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

Theorem sbceq1a 3751
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 3743 . 2 (𝑥 = 𝐴 → ([𝑥 / 𝑥]𝜑[𝐴 / 𝑥]𝜑))
31, 2bitr3id 285 1 (𝑥 = 𝐴 → (𝜑[𝐴 / 𝑥]𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1542  [wsb 2068  [wsbc 3740
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-12 2172  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-sbc 3741
This theorem is referenced by:  sbceq2a  3752  elrabsf  3788  cbvralcsf  3901  reusngf  4634  rexreusng  4641  reuprg0  4664  rmosn  4681  rabsnifsb  4684  euotd  5471  reuop  6246  frpoinsg  6298  wfisgOLD  6309  elfvmptrab1w  6975  elfvmptrab1  6976  ralrnmpt  7047  riotass2  7345  riotass  7346  oprabv  7418  elovmporab  7600  elovmporab1w  7601  elovmporab1  7602  ovmpt3rabdm  7613  elovmpt3rab1  7614  tfisg  7791  tfindes  7800  sbcopeq1a  7982  sbcoteq1a  7984  mpoxopoveq  8151  findcard2  9109  findcard2OLD  9229  ac6sfi  9232  indexfi  9305  frinsg  9688  nn0ind-raph  12604  fzrevral  13527  wrdind  14611  wrd2ind  14612  prmind2  16562  elmptrab  23181  isfildlem  23211  2sqreulem4  26805  gropd  27985  grstructd  27986  rspc2daf  31400  opreu2reuALT  31408  ifeqeqx  31467  wrdt2ind  31810  bnj919  33382  bnj976  33392  bnj1468  33461  bnj110  33473  bnj150  33491  bnj151  33492  bnj607  33531  bnj873  33539  bnj849  33540  bnj1388  33648  setinds  34356  dfon2lem1  34361  rdgssun  35852  indexdom  36196  sdclem2  36204  sdclem1  36205  fdc1  36208  riotasv2s  37423  elimhyps  37426  sbccomieg  41119  rexrabdioph  41120  rexfrabdioph  41121  aomclem6  41389  pm13.13a  42694  pm13.13b  42695  pm13.14  42696  tratrb  42825  uzwo4  43268  or2expropbilem2  45274  reuf1odnf  45346  ich2exprop  45670  ichnreuop  45671  ichreuopeq  45672  prproropreud  45708  reupr  45721  reuopreuprim  45725
  Copyright terms: Public domain W3C validator