Theorem bj-dfsb2

Description: Alternate (dual) definition of substitution df-sb not using dummy variables. (Contributed by BJ, 19-Mar-2021)

	Ref	Expression
Assertion	bj-dfsb2	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∨ ( 𝑥 = 𝑦 ∧ 𝜑 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dfsb1	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ ( ( 𝑥 = 𝑦 → 𝜑 ) ∧ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) ) )
2		bj-sbsb	⊢ ( ( ( 𝑥 = 𝑦 → 𝜑 ) ∧ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) ) ↔ ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∨ ( 𝑥 = 𝑦 ∧ 𝜑 ) ) )
3	1 2	bitri	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∨ ( 𝑥 = 𝑦 ∧ 𝜑 ) ) )