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

Theorem sbco2 2511
Description: A composition law for substitution. For versions requiring fewer axioms, but more disjoint variable conditions, see sbco2v 2327 and sbco2vv 2101. Usage of this theorem is discouraged because it depends on ax-13 2372. (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 17-Sep-2018.) (New usage is discouraged.)
Hypothesis
Ref Expression
sbco2.1 𝑧𝜑
Assertion
Ref Expression
sbco2 ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)

Proof of Theorem sbco2
StepHypRef Expression
1 sbequ12 2244 . . . 4 (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑧][𝑧 / 𝑥]𝜑))
2 sbequ 2087 . . . 4 (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑))
31, 2bitr3d 281 . . 3 (𝑧 = 𝑦 → ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑))
43sps 2179 . 2 (∀𝑧 𝑧 = 𝑦 → ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑))
5 nfnae 2434 . . 3 𝑧 ¬ ∀𝑧 𝑧 = 𝑦
6 sbco2.1 . . . 4 𝑧𝜑
76nfsb4 2500 . . 3 (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧[𝑦 / 𝑥]𝜑)
82a1i 11 . . 3 (¬ ∀𝑧 𝑧 = 𝑦 → (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)))
95, 7, 8sbied 2503 . 2 (¬ ∀𝑧 𝑧 = 𝑦 → ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑))
104, 9pm2.61i 182 1 ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wal 1540  wnf 1786  [wsb 2068
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-10 2138  ax-11 2155  ax-12 2172  ax-13 2372
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-nf 1787  df-sb 2069
This theorem is referenced by:  sbco2d  2512  sb7f  2525  cbvab  2809  clelsb2OLD  2863  clelsb1f  2909  sbcco  3804
  Copyright terms: Public domain W3C validator