Theorem bnj610

Description: Pass from equality ( x = A ) to substitution ( [. A / x ]. ) without the distinct variable condition on A , x . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj610.1	|- A e. _V
	bnj610.2	|- ( x = A -> ( ph <-> ps ) )
	bnj610.3	|- ( x = y -> ( ph <-> ps' ) )
	bnj610.4	|- ( y = A -> ( ps' <-> ps ) )
Assertion	bnj610	|- ( [. A / x ]. ph <-> ps )

Proof

Step	Hyp	Ref	Expression
1		bnj610.1	|- A e. _V
2		bnj610.2	|- ( x = A -> ( ph <-> ps ) )
3		bnj610.3	|- ( x = y -> ( ph <-> ps' ) )
4		bnj610.4	|- ( y = A -> ( ps' <-> ps ) )
5		vex	|- y e. _V
6	5 3	sbcie	|- ( [. y / x ]. ph <-> ps' )
7	6	sbcbii	|- ( [. A / y ]. [. y / x ]. ph <-> [. A / y ]. ps' )
8		sbccow	|- ( [. A / y ]. [. y / x ]. ph <-> [. A / x ]. ph )
9	1 4	sbcie	|- ( [. A / y ]. ps' <-> ps )
10	7 8 9	3bitr3i	|- ( [. A / x ]. ph <-> ps )