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

Theorem sbequ 2077
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 2076 . 2
2 sbequi 2076 . . 3
32equcoms 1735 . 2
41, 3impbid 191 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  [wsb 1702
This theorem is referenced by:  drsb2  2079  sbcom3  2115  sbco2  2121  sbco2OLD  2122  sbcom2  2160  sb10f  2175  sb8eu  2301  sb8euOLD  2302  sb8euOLDOLD  2303  cbvabOLD  2596  cbvralf  3050  cbvreu  3054  cbvralsv  3067  cbvrexsv  3068  cbvrab  3079  cbvreucsf  3435  cbvrabcsf  3436  sbss  3903  cbvopab1  4479  cbvmpt  4499  cbviota  5505  sb8iota  5507  cbvriota  6193  tfis  6598  tfinds  6603  findes  6639  uzind4s  11053  wl-sbcom2d-lem1  28845  wl-sb8eut  28858  wl-sbcom3  28871  sbeqi  29432  frege52b  36572
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-12 1794  ax-13 1955
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-nf 1591  df-sb 1703
  Copyright terms: Public domain W3C validator