This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ (φ \land x \in A) \to ψ$
	Assertion	rabeqcda	$⊢ φ \to \{x \in A \| ψ\} = A$

Proof

Step	Hyp	Ref	Expression
1		rabeqcda.1	$⊢ (φ \land x \in A) \to ψ$
2		df-rab	$⊢ \{x \in A \| ψ\} = \{x \| (x \in A \land ψ)\}$
3	1	ex	$⊢ φ \to (x \in A \to ψ)$
4	3	pm4.71d	$⊢ φ \to (x \in A \leftrightarrow (x \in A \land ψ))$
5	4	eqabdv	$⊢ φ \to A = \{x \| (x \in A \land ψ)\}$
6	2 5	eqtr4id	$⊢ φ \to \{x \in A \| ψ\} = A$