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	$$⊢\left[y/x\right]\phi \leftrightarrow \left(\forall x\left(x=y\to \phi \right)\vee \left(x=y\wedge \phi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfsb1	$$⊢\left[y/x\right]\phi \leftrightarrow \left(\left(x=y\to \phi \right)\wedge \exists x\left(x=y\wedge \phi \right)\right)$$
2		bj-sbsb	$$⊢\left(\left(x=y\to \phi \right)\wedge \exists x\left(x=y\wedge \phi \right)\right)\leftrightarrow \left(\forall x\left(x=y\to \phi \right)\vee \left(x=y\wedge \phi \right)\right)$$
3	1 2	bitri	$$⊢\left[y/x\right]\phi \leftrightarrow \left(\forall x\left(x=y\to \phi \right)\vee \left(x=y\wedge \phi \right)\right)$$