Theorem rabid2f

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

	Ref	Expression
Hypothesis	rabid2f.1	|- F/_ x A
Assertion	rabid2f	|- ( A = { x e. A | ph } <-> A. x e. A ph )

Proof

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