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