Theorem sb6OLD

Description: Obsolete version of sb6 as of 7-Jul-2023. Equivalence for substitution. Compare Theorem 6.2 of Quine p. 40. Also proved as Lemmas 16 and 17 of Tarski p. 70. The implication "to the left", sb2vOLD , 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) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	sb6OLD	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		sb4vOLD	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) )
2		sb2vOLD	⊢ ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) → [ 𝑦 / 𝑥 ] 𝜑 )
3	1 2	impbii	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) )