Theorem sb56

Description: Two equivalent ways of expressing the proper substitution of y for x in ph , when x and y are distinct, namely, alternate definitions sb5 and sb6 . Theorem 6.2 of Quine p. 40. The proof does not involve df-sb . The implication "to the left" is equs4 and does not require any disjoint variable condition (but the version with a disjoint variable condition, equs4v , requires fewer axioms). Theorem equs45f replaces the disjoint variable condition with a non-freeness hypothesis and equs5 replaces it with a distinctor as antecedent. (Contributed by NM, 14-Apr-2008) Revised to use equsexv in place of equsex in order to remove dependency on ax-13 . (Revised by BJ, 20-Dec-2020)

	Ref	Expression
Assertion	sb56	⊢ ( ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		sb5	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) )
2		sb6	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) )
3	1 2	bitr3i	⊢ ( ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) )