Metamath Proof Explorer


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 } ) )