Theorem sb5

Description: Alternate definition of substitution when variables are disjoint. Similar to Theorem 6.1 of Quine p. 40. The implication "to the right" is sb1v and even needs no disjoint variable condition, see sb1 . Theorem sb5f replaces the disjoint variable condition with a nonfreeness hypothesis. (Contributed by NM, 18-Aug-1993) (Revised by Wolf Lammen, 4-Sep-2023)

	Ref	Expression
Assertion	sb5	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) )

Proof

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