Theorem sbco2 2515

Description: A composition law for substitution. For versions requiring fewer axioms, but more disjoint variable conditions, see sbco2v 2331 and sbco2vv 2099. Usage of this theorem is discouraged because it depends on ax-13 2376. (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 2251	. . . 4 ⊢ (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑧][𝑧 / 𝑥]𝜑))
2		sbequ 2083	. . . 4 ⊢ (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑))
3	1, 2	bitr3d 281	. . 3 ⊢ (𝑧 = 𝑦 → ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑))
4	3	sps 2185	. 2 ⊢ (∀𝑧 𝑧 = 𝑦 → ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑))
5		nfnae 2438	. . 3 ⊢ Ⅎ𝑧 ¬ ∀𝑧 𝑧 = 𝑦
6		sbco2.1	. . . 4 ⊢ Ⅎ𝑧𝜑
7	6	nfsb4 2504	. . 3 ⊢ (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧[𝑦 / 𝑥]𝜑)
8	2	a1i 11	. . 3 ⊢ (¬ ∀𝑧 𝑧 = 𝑦 → (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)))
9	5, 7, 8	sbied 2507	. 2 ⊢ (¬ ∀𝑧 𝑧 = 𝑦 → ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑))
10	4, 9	pm2.61i 182	1 ⊢ ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206  ∀wal 1538  Ⅎwnf 1783  [wsb 2064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-10 2141  ax-11 2157  ax-12 2177  ax-13 2376

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2065

This theorem is referenced by:  sbco2d  2516  sb7f  2529  cbvab  2807  clelsb2OLD  2863  clelsb1f  2903  sbcco  3791