Metamath Proof Explorer


Theorem rabxfr

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

Proof

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