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	$$⊢\left(\phi \wedge x\in A\right)\to \psi$$
Assertion	rabeqcda	$$⊢\phi \to \left\{x\in A|\psi \right\}=A$$

Proof

Step	Hyp	Ref	Expression
1		rabeqcda.1	$$⊢\left(\phi \wedge x\in A\right)\to \psi$$
2		df-rab	$$⊢\left\{x\in A|\psi \right\}=\left\{x|\left(x\in A\wedge \psi \right)\right\}$$
3	1	ex	$$⊢\phi \to \left(x\in A\to \psi \right)$$
4	3	pm4.71d	$$⊢\phi \to \left(x\in A\leftrightarrow \left(x\in A\wedge \psi \right)\right)$$
5	4	bicomd	$$⊢\phi \to \left(\left(x\in A\wedge \psi \right)\leftrightarrow x\in A\right)$$
6	5	abbi1dv	$$⊢\phi \to \left\{x|\left(x\in A\wedge \psi \right)\right\}=A$$
7	2 6	eqtrid	$$⊢\phi \to \left\{x\in A|\psi \right\}=A$$