Theorem sbco2 2540

Description: A composition law for substitution. For versions requiring fewer axioms, but more disjoint variable conditions, see sbco2v 2361 and sbco2vv 2135. Usage of this theorem is discouraged because it depends on ax-13 2401. (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

Step	Hyp	Ref	Expression
1		sbequ12 2286	. . . 4 ⊢ (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑧][𝑧 / 𝑥]𝜑))
2		sbequ 2119	. . . 4 ⊢ (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑))
3	1, 2	bitr3d 284	. . 3 ⊢ (𝑧 = 𝑦 → ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑))
4	3	sps 2221	. 2 ⊢ (∀𝑧 𝑧 = 𝑦 → ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑))
5		nfnae 2463	. . 3 ⊢ Ⅎ𝑧 ¬ ∀𝑧 𝑧 = 𝑦
6		sbco2.1	. . . 4 ⊢ Ⅎ𝑧𝜑
7	6	nfsb4 2529	. . 3 ⊢ (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧[𝑦 / 𝑥]𝜑)
8	2	a1i 11	. . 3 ⊢ (¬ ∀𝑧 𝑧 = 𝑦 → (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)))
9	5, 7, 8	sbied 2532	. 2 ⊢ (¬ ∀𝑧 𝑧 = 𝑦 → ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑))
10	4, 9	pm2.61i 184	1 ⊢ ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209  ∀wal 1567  Ⅎwnf 1815  [wsb 2098

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-10 2177  ax-11 2193  ax-12 2212  ax-13 2401

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-nf 1816  df-sb 2099

This theorem is used by:  sbco2d  2541  sb7f  2554  cbvab  2832  clelsb1f  2927  sbcco  3764