Theorem rababg

Description: Condition when restricted class is equal to unrestricted class. (Contributed by RP, 13-Aug-2020)

	Ref	Expression
Assertion	rababg	|- ( A. x ( ph -> x e. A ) <-> { x e. A | ph } = { x | ph } )

Proof

Step	Hyp	Ref	Expression
1		ancrb	|- ( ( ph -> x e. A ) <-> ( ph -> ( x e. A /\ ph ) ) )
2	1	albii	|- ( A. x ( ph -> x e. A ) <-> A. x ( ph -> ( x e. A /\ ph ) ) )
3		nfv	|- F/ y ( ph -> ( x e. A /\ ph ) )
4		nfsab1	|- F/ x y e. { x | ph }
5		nfrab1	|- F/_ x { x e. A | ph }
6	5	nfcri	|- F/ x y e. { x e. A | ph }
7	4 6	nfim	|- F/ x ( y e. { x | ph } -> y e. { x e. A | ph } )
8		abid	|- ( x e. { x | ph } <-> ph )
9		eleq1w	|- ( x = y -> ( x e. { x | ph } <-> y e. { x | ph } ) )
10	8 9	bitr3id	|- ( x = y -> ( ph <-> y e. { x | ph } ) )
11		rabid	|- ( x e. { x e. A | ph } <-> ( x e. A /\ ph ) )
12		eleq1w	|- ( x = y -> ( x e. { x e. A | ph } <-> y e. { x e. A | ph } ) )
13	11 12	bitr3id	|- ( x = y -> ( ( x e. A /\ ph ) <-> y e. { x e. A | ph } ) )
14	10 13	imbi12d	|- ( x = y -> ( ( ph -> ( x e. A /\ ph ) ) <-> ( y e. { x | ph } -> y e. { x e. A | ph } ) ) )
15	3 7 14	cbvalv1	|- ( A. x ( ph -> ( x e. A /\ ph ) ) <-> A. y ( y e. { x | ph } -> y e. { x e. A | ph } ) )
16		eqss	|- ( { x e. A | ph } = { x | ph } <-> ( { x e. A | ph } C_ { x | ph } /\ { x | ph } C_ { x e. A | ph } ) )
17		rabssab	|- { x e. A | ph } C_ { x | ph }
18	17	biantrur	|- ( { x | ph } C_ { x e. A | ph } <-> ( { x e. A | ph } C_ { x | ph } /\ { x | ph } C_ { x e. A | ph } ) )
19		df-ss	|- ( { x | ph } C_ { x e. A | ph } <-> A. y ( y e. { x | ph } -> y e. { x e. A | ph } ) )
20	16 18 19	3bitr2ri	|- ( A. y ( y e. { x | ph } -> y e. { x e. A | ph } ) <-> { x e. A | ph } = { x | ph } )
21	2 15 20	3bitri	|- ( A. x ( ph -> x e. A ) <-> { x e. A | ph } = { x | ph } )