Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  sbequ Unicode version

Theorem sbequ 2013
 Description: An equality theorem for substitution. Used in proof of Theorem 9.7 in [Megill] p. 449 (p. 16 of the preprint). (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
sbequ

Proof of Theorem sbequ
StepHypRef Expression
1 sbequi 2012 . 2
2 sbequi 2012 . . 3
32equcoms 1666 . 2
41, 3impbid 183 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 176  wsb 1638 This theorem is referenced by:  drsb2  2014  sbco2  2039  sb10f  2074  sb8eu  2174  cbvab  2414  cbvralf  2771  cbvreu  2775  cbvralsv  2788  cbvrexsv  2789  cbvrab  2799  cbvreucsf  3158  cbvrabcsf  3159  sbss  3576  cbvopab1  4105  cbvmpt  4126  tfis  4661  tfisi  4665  tfinds  4666  findes  4702  cbviota  5240  sb8iota  5242  cbvriota  6331  uzind4s  10294  cbvmptf  23235 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639
 Copyright terms: Public domain W3C validator