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 ( 𝑥𝐴𝜑 )
Assertion rabeqc { 𝑥𝐴𝜑 } = 𝐴

Proof

Step Hyp Ref Expression
1 rabeqc.1 ( 𝑥𝐴𝜑 )
2 1 adantl ( ( ⊤ ∧ 𝑥𝐴 ) → 𝜑 )
3 2 rabeqcda ( ⊤ → { 𝑥𝐴𝜑 } = 𝐴 )
4 3 mptru { 𝑥𝐴𝜑 } = 𝐴