Theorem sb6

Description: Alternate definition of substitution when variables are disjoint. Compare Theorem 6.2 of Quine p. 40. Also proved as Lemmas 16 and 17 of Tarski p. 70. The implication "to the left" also holds without a disjoint variable condition ( sb2 ). Theorem sb6f replaces the disjoint variable condition with a non-freeness hypothesis. Theorem sb4b replaces it with a distinctor antecedent. (Contributed by NM, 18-Aug-1993) (Proof shortened by Wolf Lammen, 21-Sep-2018) Revise df-sb . (Revised by BJ, 22-Dec-2020) Remove use of ax-11 . (Revised by Steven Nguyen, 7-Jul-2023) (Proof shortened by Wolf Lammen, 16-Jul-2023)

	Ref	Expression
Assertion	sb6	⊢ ( [ 𝑡 / 𝑥 ] 𝜑 ↔ ∀ 𝑥 ( 𝑥 = 𝑡 → 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		df-sb	⊢ ( [ 𝑡 / 𝑥 ] 𝜑 ↔ ∀ 𝑦 ( 𝑦 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )
2		equequ2	⊢ ( 𝑦 = 𝑡 → ( 𝑥 = 𝑦 ↔ 𝑥 = 𝑡 ) )
3	2	imbi1d	⊢ ( 𝑦 = 𝑡 → ( ( 𝑥 = 𝑦 → 𝜑 ) ↔ ( 𝑥 = 𝑡 → 𝜑 ) ) )
4	3	albidv	⊢ ( 𝑦 = 𝑡 → ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 = 𝑡 → 𝜑 ) ) )
5	4	equsalvw	⊢ ( ∀ 𝑦 ( 𝑦 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ↔ ∀ 𝑥 ( 𝑥 = 𝑡 → 𝜑 ) )
6	1 5	bitri	⊢ ( [ 𝑡 / 𝑥 ] 𝜑 ↔ ∀ 𝑥 ( 𝑥 = 𝑡 → 𝜑 ) )