Theorem sbcom3

Description: Substituting y for x and then z for y is equivalent to substituting z for both x and y . Usage of this theorem is discouraged because it depends on ax-13 . For a version requiring a disjoint variable, but fewer axioms, see sbcom3vv . (Contributed by Giovanni Mascellani, 8-Apr-2018) Remove dependency on ax-11 . (Revised by Wolf Lammen, 16-Sep-2018) (Proof shortened by Wolf Lammen, 16-Sep-2018) (New usage is discouraged.)

	Ref	Expression
Assertion	sbcom3	⊢ ( [ 𝑧 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑧 / 𝑦 ] [ 𝑧 / 𝑥 ] 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		nfa1	⊢ Ⅎ 𝑦 ∀ 𝑦 𝑦 = 𝑧
2		drsb2	⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑧 / 𝑥 ] 𝜑 ) )
3	1 2	sbbid	⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ( [ 𝑧 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑧 / 𝑦 ] [ 𝑧 / 𝑥 ] 𝜑 ) )
4		sb4b	⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ( [ 𝑧 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ ∀ 𝑦 ( 𝑦 = 𝑧 → [ 𝑦 / 𝑥 ] 𝜑 ) ) )
5		sbequ	⊢ ( 𝑦 = 𝑧 → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑧 / 𝑥 ] 𝜑 ) )
6	5	pm5.74i	⊢ ( ( 𝑦 = 𝑧 → [ 𝑦 / 𝑥 ] 𝜑 ) ↔ ( 𝑦 = 𝑧 → [ 𝑧 / 𝑥 ] 𝜑 ) )
7	6	albii	⊢ ( ∀ 𝑦 ( 𝑦 = 𝑧 → [ 𝑦 / 𝑥 ] 𝜑 ) ↔ ∀ 𝑦 ( 𝑦 = 𝑧 → [ 𝑧 / 𝑥 ] 𝜑 ) )
8	4 7	bitrdi	⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ( [ 𝑧 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ ∀ 𝑦 ( 𝑦 = 𝑧 → [ 𝑧 / 𝑥 ] 𝜑 ) ) )
9		sb4b	⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ( [ 𝑧 / 𝑦 ] [ 𝑧 / 𝑥 ] 𝜑 ↔ ∀ 𝑦 ( 𝑦 = 𝑧 → [ 𝑧 / 𝑥 ] 𝜑 ) ) )
10	8 9	bitr4d	⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ( [ 𝑧 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑧 / 𝑦 ] [ 𝑧 / 𝑥 ] 𝜑 ) )
11	3 10	pm2.61i	⊢ ( [ 𝑧 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑧 / 𝑦 ] [ 𝑧 / 𝑥 ] 𝜑 )