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 non-freeness hypothesis. (Contributed by NM, 18-Aug-1993) Shorten sb56 . (Revised by Wolf Lammen, 4-Sep-2023)

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

Proof

Step	Hyp	Ref	Expression
1		nfs1v	⊢ Ⅎ 𝑥 [ 𝑦 / 𝑥 ] 𝜑
2		sbequ12	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) )
3	1 2	equsexv	⊢ ( ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) ↔ [ 𝑦 / 𝑥 ] 𝜑 )
4	3	bicomi	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) )