This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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