Theorem bnj1468

Description: Conversion of implicit substitution to explicit class substitution. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		bnj1468.1	|- ( ps -> A. x ps )
2		bnj1468.2	|- ( x = A -> ( ph <-> ps ) )
3		bnj1468.3	|- ( y e. A -> A. x y e. A )
4		sbccow	|- ( [. A / y ]. [. y / x ]. ph <-> [. A / x ]. ph )
5		ax-5	|- ( ps -> A. y ps )
6	3	nfcii	|- F/_ x A
7	6	nfeq2	|- F/ x y = A
8		nfsbc1v	|- F/ x [. y / x ]. ph
9	1	nf5i	|- F/ x ps
10	8 9	nfbi	|- F/ x ( [. y / x ]. ph <-> ps )
11	7 10	nfim	|- F/ x ( y = A -> ( [. y / x ]. ph <-> ps ) )
12	11	nf5ri	|- ( ( y = A -> ( [. y / x ]. ph <-> ps ) ) -> A. x ( y = A -> ( [. y / x ]. ph <-> ps ) ) )
13		ax6ev	|- E. x x = y
14		eqeq1	|- ( x = y -> ( x = A <-> y = A ) )
15	14 2	syl6bir	|- ( x = y -> ( y = A -> ( ph <-> ps ) ) )
16		sbceq1a	|- ( x = y -> ( ph <-> [. y / x ]. ph ) )
17	16	bibi1d	|- ( x = y -> ( ( ph <-> ps ) <-> ( [. y / x ]. ph <-> ps ) ) )
18	15 17	sylibd	|- ( x = y -> ( y = A -> ( [. y / x ]. ph <-> ps ) ) )
19	13 18	bnj101	|- E. x ( y = A -> ( [. y / x ]. ph <-> ps ) )
20	12 19	bnj1131	|- ( y = A -> ( [. y / x ]. ph <-> ps ) )
21	5 20	bnj1464	|- ( A e. V -> ( [. A / y ]. [. y / x ]. ph <-> ps ) )
22	4 21	bitr3id	|- ( A e. V -> ( [. A / x ]. ph <-> ps ) )