Theorem rabxfrd

Description: Membership in a restricted class abstraction after substituting an expression A (containing y ) for x in the formula defining the class abstraction. (Contributed by NM, 16-Jan-2012)

	Ref	Expression
Hypotheses	rabxfrd.1	|- F/_ y B
	rabxfrd.2	|- F/_ y C
	rabxfrd.3	|- ( ( ph /\ y e. D ) -> A e. D )
	rabxfrd.4	|- ( x = A -> ( ps <-> ch ) )
	rabxfrd.5	|- ( y = B -> A = C )
Assertion	rabxfrd	|- ( ( ph /\ B e. D ) -> ( C e. { x e. D | ps } <-> B e. { y e. D | ch } ) )

Proof

Step	Hyp	Ref	Expression
1		rabxfrd.1	|- F/_ y B
2		rabxfrd.2	|- F/_ y C
3		rabxfrd.3	|- ( ( ph /\ y e. D ) -> A e. D )
4		rabxfrd.4	|- ( x = A -> ( ps <-> ch ) )
5		rabxfrd.5	|- ( y = B -> A = C )
6	3	ex	|- ( ph -> ( y e. D -> A e. D ) )
7		ibibr	|- ( ( y e. D -> A e. D ) <-> ( y e. D -> ( A e. D <-> y e. D ) ) )
8	6 7	sylib	|- ( ph -> ( y e. D -> ( A e. D <-> y e. D ) ) )
9	8	imp	|- ( ( ph /\ y e. D ) -> ( A e. D <-> y e. D ) )
10	9	anbi1d	|- ( ( ph /\ y e. D ) -> ( ( A e. D /\ ch ) <-> ( y e. D /\ ch ) ) )
11	4	elrab	|- ( A e. { x e. D | ps } <-> ( A e. D /\ ch ) )
12		rabid	|- ( y e. { y e. D | ch } <-> ( y e. D /\ ch ) )
13	10 11 12	3bitr4g	|- ( ( ph /\ y e. D ) -> ( A e. { x e. D | ps } <-> y e. { y e. D | ch } ) )
14	13	rabbidva	|- ( ph -> { y e. D | A e. { x e. D | ps } } = { y e. D | y e. { y e. D | ch } } )
15	14	eleq2d	|- ( ph -> ( B e. { y e. D | A e. { x e. D | ps } } <-> B e. { y e. D | y e. { y e. D | ch } } ) )
16		nfcv	|- F/_ y D
17	2	nfel1	|- F/ y C e. { x e. D | ps }
18	5	eleq1d	|- ( y = B -> ( A e. { x e. D | ps } <-> C e. { x e. D | ps } ) )
19	1 16 17 18	elrabf	|- ( B e. { y e. D | A e. { x e. D | ps } } <-> ( B e. D /\ C e. { x e. D | ps } ) )
20		nfrab1	|- F/_ y { y e. D | ch }
21	1 20	nfel	|- F/ y B e. { y e. D | ch }
22		eleq1	|- ( y = B -> ( y e. { y e. D | ch } <-> B e. { y e. D | ch } ) )
23	1 16 21 22	elrabf	|- ( B e. { y e. D | y e. { y e. D | ch } } <-> ( B e. D /\ B e. { y e. D | ch } ) )
24	15 19 23	3bitr3g	|- ( ph -> ( ( B e. D /\ C e. { x e. D | ps } ) <-> ( B e. D /\ B e. { y e. D | ch } ) ) )
25		pm5.32	|- ( ( B e. D -> ( C e. { x e. D | ps } <-> B e. { y e. D | ch } ) ) <-> ( ( B e. D /\ C e. { x e. D | ps } ) <-> ( B e. D /\ B e. { y e. D | ch } ) ) )
26	24 25	sylibr	|- ( ph -> ( B e. D -> ( C e. { x e. D | ps } <-> B e. { y e. D | ch } ) ) )
27	26	imp	|- ( ( ph /\ B e. D ) -> ( C e. { x e. D | ps } <-> B e. { y e. D | ch } ) )