Theorem eqrabi

Description: Class element of a restricted class abstraction. (Contributed by Peter Mazsa, 24-Jul-2021)

	Ref	Expression
Hypothesis	eqrabi.1	|- ( x e. A <-> ( x e. B /\ ph ) )
Assertion	eqrabi	|- A = { x e. B | ph }

Proof

Step	Hyp	Ref	Expression
1		eqrabi.1	|- ( x e. A <-> ( x e. B /\ ph ) )
2	1	eqabi	|- A = { x | ( x e. B /\ ph ) }
3		df-rab	|- { x e. B | ph } = { x | ( x e. B /\ ph ) }
4	2 3	eqtr4i	|- A = { x e. B | ph }