Description: Membership in a restricted class abstraction after substituting an expression A (containing y ) for x in the the formula defining the class abstraction. (Contributed by NM, 10-Jun-2005)
Ref | Expression | ||
---|---|---|---|
Hypotheses | rabxfr.1 | |- F/_ y B |
|
rabxfr.2 | |- F/_ y C |
||
rabxfr.3 | |- ( y e. D -> A e. D ) |
||
rabxfr.4 | |- ( x = A -> ( ph <-> ps ) ) |
||
rabxfr.5 | |- ( y = B -> A = C ) |
||
Assertion | rabxfr | |- ( B e. D -> ( C e. { x e. D | ph } <-> B e. { y e. D | ps } ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rabxfr.1 | |- F/_ y B |
|
2 | rabxfr.2 | |- F/_ y C |
|
3 | rabxfr.3 | |- ( y e. D -> A e. D ) |
|
4 | rabxfr.4 | |- ( x = A -> ( ph <-> ps ) ) |
|
5 | rabxfr.5 | |- ( y = B -> A = C ) |
|
6 | tru | |- T. |
|
7 | 3 | adantl | |- ( ( T. /\ y e. D ) -> A e. D ) |
8 | 1 2 7 4 5 | rabxfrd | |- ( ( T. /\ B e. D ) -> ( C e. { x e. D | ph } <-> B e. { y e. D | ps } ) ) |
9 | 6 8 | mpan | |- ( B e. D -> ( C e. { x e. D | ph } <-> B e. { y e. D | ps } ) ) |