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

Theorem sbequ 2111
 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 2110 . 2
2 sbequi 2110 . . 3
32equcoms 1693 . 2
41, 3impbid 184 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177  wsb 1658 This theorem is referenced by:  drsb2  2113  sbco2  2161  sb10f  2199  sb8eu  2299  cbvab  2554  cbvralf  2926  cbvreu  2930  cbvralsv  2943  cbvrexsv  2944  cbvrab  2954  cbvreucsf  3313  cbvrabcsf  3314  sbss  3737  cbvopab1  4278  cbvmpt  4299  tfis  4834  tfinds  4839  findes  4875  cbviota  5423  sb8iota  5425  cbvriota  6560  uzind4s  10536 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950 This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659
 Copyright terms: Public domain W3C validator