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	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝜓 )
Assertion	rabeqcda	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝜓 } = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		rabeqcda.1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝜓 )
2		df-rab	⊢ { 𝑥 ∈ 𝐴 ∣ 𝜓 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) }
3	1	ex	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → 𝜓 ) )
4	3	pm4.71d	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) )
5	4	eqabdv	⊢ ( 𝜑 → 𝐴 = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) } )
6	2 5	eqtr4id	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝜓 } = 𝐴 )