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

Theorem sbequ 2117
 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, 14-May-1993.)
Assertion
Ref Expression
sbequ

Proof of Theorem sbequ
StepHypRef Expression
1 sbequi 2116 . 2
2 sbequi 2116 . . 3
32equcoms 1795 . 2
41, 3impbid 191 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  <->wb 184  [wsb 1739 This theorem is referenced by:  drsb2  2119  sbcom3  2153  sbco2  2158  sbcom2  2189  sb10f  2200  sb8eu  2318  sb8euOLD  2319  cbvabOLD  2599  cbvralf  3078  cbvreu  3082  cbvralsv  3095  cbvrexsv  3096  cbvrab  3107  cbvreucsf  3468  cbvrabcsf  3469  sbss  3939  cbvopab1  4522  cbvmpt  4542  cbviota  5561  sb8iota  5563  cbvriota  6267  tfis  6689  tfinds  6694  findes  6730  uzind4s  11170  wl-sbcom2d-lem1  30009  wl-sb8eut  30022  wl-sbcom3  30035  sbeqi  30568 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-12 1854  ax-13 1999 This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-nf 1617  df-sb 1740
 Copyright terms: Public domain W3C validator