Theorem rabeqc

Description: A restricted class abstraction equals the restricting class if its condition follows from the membership of the free setvar variable in the restricting class. (Contributed by AV, 20-Apr-2022)

	Ref	Expression
Hypothesis	rabeqc.1	|- ( x e. A -> ph )
Assertion	rabeqc	|- { x e. A | ph } = A

Proof

Step	Hyp	Ref	Expression
1		rabeqc.1	|- ( x e. A -> ph )
2		df-rab	|- { x e. A | ph } = { x | ( x e. A /\ ph ) }
3		abeq1	|- ( { x | ( x e. A /\ ph ) } = A <-> A. x ( ( x e. A /\ ph ) <-> x e. A ) )
4	1	pm4.71i	|- ( x e. A <-> ( x e. A /\ ph ) )
5	4	bicomi	|- ( ( x e. A /\ ph ) <-> x e. A )
6	3 5	mpgbir	|- { x | ( x e. A /\ ph ) } = A
7	2 6	eqtri	|- { x e. A | ph } = A