Theorem rabid2

Description: An "identity" law for restricted class abstraction. (Contributed by NM, 9-Oct-2003) (Proof shortened by Andrew Salmon, 30-May-2011)

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

Proof

Step	Hyp	Ref	Expression
1		abeq2	|- ( A = { x | ( x e. A /\ ph ) } <-> A. x ( x e. A <-> ( x e. A /\ ph ) ) )
2		pm4.71	|- ( ( x e. A -> ph ) <-> ( x e. A <-> ( x e. A /\ ph ) ) )
3	2	albii	|- ( A. x ( x e. A -> ph ) <-> A. x ( x e. A <-> ( x e. A /\ ph ) ) )
4	1 3	bitr4i	|- ( A = { x | ( x e. A /\ ph ) } <-> A. x ( x e. A -> ph ) )
5		df-rab	|- { x e. A | ph } = { x | ( x e. A /\ ph ) }
6	5	eqeq2i	|- ( A = { x e. A | ph } <-> A = { x | ( x e. A /\ ph ) } )
7		df-ral	|- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
8	4 6 7	3bitr4i	|- ( A = { x e. A | ph } <-> A. x e. A ph )