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\in \mathrm{V}$$
	bnj610.2	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
	bnj610.3	No typesetting found for |- ( x = y -> ( ph <-> ps' ) ) with typecode |-
	bnj610.4	No typesetting found for |- ( y = A -> ( ps' <-> ps ) ) with typecode |-
Assertion	bnj610	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \psi$$

Proof

Step	Hyp	Ref	Expression
1		bnj610.1	$$⊢A\in \mathrm{V}$$
2		bnj610.2	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
3		bnj610.3	Could not format ( x = y -> ( ph <-> ps' ) ) : No typesetting found for |- ( x = y -> ( ph <-> ps' ) ) with typecode |-
4		bnj610.4	Could not format ( y = A -> ( ps' <-> ps ) ) : No typesetting found for |- ( y = A -> ( ps' <-> ps ) ) with typecode |-
5		vex	$$⊢y\in \mathrm{V}$$
6	5 3	sbcie	Could not format ( [. y / x ]. ph <-> ps' ) : No typesetting found for |- ( [. y / x ]. ph <-> ps' ) with typecode |-
7	6	sbcbii	Could not format ( [. A / y ]. [. y / x ]. ph <-> [. A / y ]. ps' ) : No typesetting found for |- ( [. A / y ]. [. y / x ]. ph <-> [. A / y ]. ps' ) with typecode |-
8		sbccow	$$⊢\underset{\dot{}}{[}A/y\underset{\dot{}}{]}\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$
9	1 4	sbcie	Could not format ( [. A / y ]. ps' <-> ps ) : No typesetting found for |- ( [. A / y ]. ps' <-> ps ) with typecode |-
10	7 8 9	3bitr3i	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \psi$$