This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sbco2

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

Ref Expression
Hypothesis sbco2.1 ⊢ Ⅎ 𝑧 𝜑
Assertion sbco2 ( [ 𝑦 / 𝑧 ] [ 𝑧 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 )

Proof

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