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

Theorem equsb3 2510
 Description: Substitution in an equality. For a version requiring disjoint variables, but fewer axioms, see equsb3v 2291. (Contributed by Raph Levien and FL, 4-Dec-2005.) Remove dependency on ax-11 2150. (Revised by Wolf Lammen, 21-Sep-2018.)
Assertion
Ref Expression
equsb3 ([𝑥 / 𝑦]𝑦 = 𝑧𝑥 = 𝑧)
Distinct variable group:   𝑦,𝑧

Proof of Theorem equsb3
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 sbcom3 2487 . . 3 ([𝑥 / 𝑤][𝑤 / 𝑦]𝑦 = 𝑧 ↔ [𝑥 / 𝑤][𝑥 / 𝑦]𝑦 = 𝑧)
2 equsb3v 2291 . . . 4 ([𝑤 / 𝑦]𝑦 = 𝑧𝑤 = 𝑧)
32sbbii 2019 . . 3 ([𝑥 / 𝑤][𝑤 / 𝑦]𝑦 = 𝑧 ↔ [𝑥 / 𝑤]𝑤 = 𝑧)
4 nfv 1957 . . . 4 𝑤[𝑥 / 𝑦]𝑦 = 𝑧
54sbf 2456 . . 3 ([𝑥 / 𝑤][𝑥 / 𝑦]𝑦 = 𝑧 ↔ [𝑥 / 𝑦]𝑦 = 𝑧)
61, 3, 53bitr3i 293 . 2 ([𝑥 / 𝑤]𝑤 = 𝑧 ↔ [𝑥 / 𝑦]𝑦 = 𝑧)
7 equsb3v 2291 . 2 ([𝑥 / 𝑤]𝑤 = 𝑧𝑥 = 𝑧)
86, 7bitr3i 269 1 ([𝑥 / 𝑦]𝑦 = 𝑧𝑥 = 𝑧)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 198  [wsb 2011 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-10 2135  ax-12 2163  ax-13 2334 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-ex 1824  df-nf 1828  df-sb 2012 This theorem is referenced by:  mo3OLD  2581  sb8iota  6108  mo5f  29913  mptsnunlem  33788  wl-equsb3  33939  wl-mo3t  33959  wl-sb8eut  33960  frege55lem1b  39159  sbeqal1  39568
 Copyright terms: Public domain W3C validator