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	|- ( [ y / x ] ph <-> ( A. x ( x = y -> ph ) \/ ( x = y /\ ph ) ) )

Proof

Step	Hyp	Ref	Expression
1		dfsb1	|- ( [ y / x ] ph <-> ( ( x = y -> ph ) /\ E. x ( x = y /\ ph ) ) )
2		bj-sbsb	|- ( ( ( x = y -> ph ) /\ E. x ( x = y /\ ph ) ) <-> ( A. x ( x = y -> ph ) \/ ( x = y /\ ph ) ) )
3	1 2	bitri	|- ( [ y / x ] ph <-> ( A. x ( x = y -> ph ) \/ ( x = y /\ ph ) ) )