Theorem rabeqcda

Description: When ps is always true in a context, a restricted class abstraction is equal to the restricting class. Deduction form of rabeqc . (Contributed by Steven Nguyen, 7-Jun-2023)

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

Proof

Step	Hyp	Ref	Expression
1		rabeqcda.1	|- ( ( ph /\ x e. A ) -> ps )
2		df-rab	|- { x e. A | ps } = { x | ( x e. A /\ ps ) }
3	1	ex	|- ( ph -> ( x e. A -> ps ) )
4	3	pm4.71d	|- ( ph -> ( x e. A <-> ( x e. A /\ ps ) ) )
5	4	bicomd	|- ( ph -> ( ( x e. A /\ ps ) <-> x e. A ) )
6	5	abbi1dv	|- ( ph -> { x | ( x e. A /\ ps ) } = A )
7	2 6	eqtrid	|- ( ph -> { x e. A | ps } = A )