Theorem sbcabel

Description: Interchange class substitution and class abstraction. (Contributed by NM, 5-Nov-2005)

	Ref	Expression
Hypothesis	sbcabel.1	|- F/_ x B
Assertion	sbcabel	|- ( A e. V -> ( [. A / x ]. { y | ph } e. B <-> { y | [. A / x ]. ph } e. B ) )

Proof

Step	Hyp	Ref	Expression
1		sbcabel.1	|- F/_ x B
2		elex	|- ( A e. V -> A e. _V )
3		sbcex2	|- ( [. A / x ]. E. w ( w = { y | ph } /\ w e. B ) <-> E. w [. A / x ]. ( w = { y | ph } /\ w e. B ) )
4		sbcan	|- ( [. A / x ]. ( w = { y | ph } /\ w e. B ) <-> ( [. A / x ]. w = { y | ph } /\ [. A / x ]. w e. B ) )
5		sbcal	|- ( [. A / x ]. A. y ( y e. w <-> ph ) <-> A. y [. A / x ]. ( y e. w <-> ph ) )
6		sbcbig	|- ( A e. _V -> ( [. A / x ]. ( y e. w <-> ph ) <-> ( [. A / x ]. y e. w <-> [. A / x ]. ph ) ) )
7		sbcg	|- ( A e. _V -> ( [. A / x ]. y e. w <-> y e. w ) )
8	7	bibi1d	|- ( A e. _V -> ( ( [. A / x ]. y e. w <-> [. A / x ]. ph ) <-> ( y e. w <-> [. A / x ]. ph ) ) )
9	6 8	bitrd	|- ( A e. _V -> ( [. A / x ]. ( y e. w <-> ph ) <-> ( y e. w <-> [. A / x ]. ph ) ) )
10	9	albidv	|- ( A e. _V -> ( A. y [. A / x ]. ( y e. w <-> ph ) <-> A. y ( y e. w <-> [. A / x ]. ph ) ) )
11	5 10	bitrid	|- ( A e. _V -> ( [. A / x ]. A. y ( y e. w <-> ph ) <-> A. y ( y e. w <-> [. A / x ]. ph ) ) )
12		abeq2	|- ( w = { y | ph } <-> A. y ( y e. w <-> ph ) )
13	12	sbcbii	|- ( [. A / x ]. w = { y | ph } <-> [. A / x ]. A. y ( y e. w <-> ph ) )
14		abeq2	|- ( w = { y | [. A / x ]. ph } <-> A. y ( y e. w <-> [. A / x ]. ph ) )
15	11 13 14	3bitr4g	|- ( A e. _V -> ( [. A / x ]. w = { y | ph } <-> w = { y | [. A / x ]. ph } ) )
16	1	nfcri	|- F/ x w e. B
17	16	sbcgf	|- ( A e. _V -> ( [. A / x ]. w e. B <-> w e. B ) )
18	15 17	anbi12d	|- ( A e. _V -> ( ( [. A / x ]. w = { y | ph } /\ [. A / x ]. w e. B ) <-> ( w = { y | [. A / x ]. ph } /\ w e. B ) ) )
19	4 18	bitrid	|- ( A e. _V -> ( [. A / x ]. ( w = { y | ph } /\ w e. B ) <-> ( w = { y | [. A / x ]. ph } /\ w e. B ) ) )
20	19	exbidv	|- ( A e. _V -> ( E. w [. A / x ]. ( w = { y | ph } /\ w e. B ) <-> E. w ( w = { y | [. A / x ]. ph } /\ w e. B ) ) )
21	3 20	bitrid	|- ( A e. _V -> ( [. A / x ]. E. w ( w = { y | ph } /\ w e. B ) <-> E. w ( w = { y | [. A / x ]. ph } /\ w e. B ) ) )
22		dfclel	|- ( { y | ph } e. B <-> E. w ( w = { y | ph } /\ w e. B ) )
23	22	sbcbii	|- ( [. A / x ]. { y | ph } e. B <-> [. A / x ]. E. w ( w = { y | ph } /\ w e. B ) )
24		dfclel	|- ( { y | [. A / x ]. ph } e. B <-> E. w ( w = { y | [. A / x ]. ph } /\ w e. B ) )
25	21 23 24	3bitr4g	|- ( A e. _V -> ( [. A / x ]. { y | ph } e. B <-> { y | [. A / x ]. ph } e. B ) )
26	2 25	syl	|- ( A e. V -> ( [. A / x ]. { y | ph } e. B <-> { y | [. A / x ]. ph } e. B ) )