Metamath Proof Explorer


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 A φ
Assertion rabeqc x A | φ = A

Proof

Step Hyp Ref Expression
1 rabeqc.1 x A φ
2 1 adantl x A φ
3 2 rabeqcda x A | φ = A
4 3 mptru x A | φ = A