Theorem sbcralt

Description: Interchange class substitution and restricted quantifier. (Contributed by NM, 1-Mar-2008) (Revised by David Abernethy, 22-Feb-2010)

	Ref	Expression
Assertion	sbcralt	|- ( ( A e. V /\ F/_ y A ) -> ( [. A / x ]. A. y e. B ph <-> A. y e. B [. A / x ]. ph ) )

Proof

Step	Hyp	Ref	Expression
1		sbccow	|- ( [. A / z ]. [. z / x ]. A. y e. B ph <-> [. A / x ]. A. y e. B ph )
2		simpl	|- ( ( A e. V /\ F/_ y A ) -> A e. V )
3		sbsbc	|- ( [ z / x ] A. y e. B ph <-> [. z / x ]. A. y e. B ph )
4		nfcv	|- F/_ x B
5		nfs1v	|- F/ x [ z / x ] ph
6	4 5	nfralw	|- F/ x A. y e. B [ z / x ] ph
7		sbequ12	|- ( x = z -> ( ph <-> [ z / x ] ph ) )
8	7	ralbidv	|- ( x = z -> ( A. y e. B ph <-> A. y e. B [ z / x ] ph ) )
9	6 8	sbiev	|- ( [ z / x ] A. y e. B ph <-> A. y e. B [ z / x ] ph )
10	3 9	bitr3i	|- ( [. z / x ]. A. y e. B ph <-> A. y e. B [ z / x ] ph )
11		nfnfc1	|- F/ y F/_ y A
12		nfcvd	|- ( F/_ y A -> F/_ y z )
13		id	|- ( F/_ y A -> F/_ y A )
14	12 13	nfeqd	|- ( F/_ y A -> F/ y z = A )
15	11 14	nfan1	|- F/ y ( F/_ y A /\ z = A )
16		dfsbcq2	|- ( z = A -> ( [ z / x ] ph <-> [. A / x ]. ph ) )
17	16	adantl	|- ( ( F/_ y A /\ z = A ) -> ( [ z / x ] ph <-> [. A / x ]. ph ) )
18	15 17	ralbid	|- ( ( F/_ y A /\ z = A ) -> ( A. y e. B [ z / x ] ph <-> A. y e. B [. A / x ]. ph ) )
19	18	adantll	|- ( ( ( A e. V /\ F/_ y A ) /\ z = A ) -> ( A. y e. B [ z / x ] ph <-> A. y e. B [. A / x ]. ph ) )
20	10 19	syl5bb	|- ( ( ( A e. V /\ F/_ y A ) /\ z = A ) -> ( [. z / x ]. A. y e. B ph <-> A. y e. B [. A / x ]. ph ) )
21	2 20	sbcied	|- ( ( A e. V /\ F/_ y A ) -> ( [. A / z ]. [. z / x ]. A. y e. B ph <-> A. y e. B [. A / x ]. ph ) )
22	1 21	bitr3id	|- ( ( A e. V /\ F/_ y A ) -> ( [. A / x ]. A. y e. B ph <-> A. y e. B [. A / x ]. ph ) )