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

Proof

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