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) (Proof shortened by SN, 15-Jan-2025)

	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	1	adantl	|- ( ( T. /\ x e. A ) -> ph )
3	2	rabeqcda	|- ( T. -> { x e. A | ph } = A )
4	3	mptru	|- { x e. A | ph } = A