Metamath Proof Explorer


Theorem rabeqcOLD

Description: Obsolete version of rabeqc as of 15-Jan-2025. (Contributed by AV, 20-Apr-2022) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis rabeqcOLD.1 ( 𝑥𝐴𝜑 )
Assertion rabeqcOLD { 𝑥𝐴𝜑 } = 𝐴

Proof

Step Hyp Ref Expression
1 rabeqcOLD.1 ( 𝑥𝐴𝜑 )
2 df-rab { 𝑥𝐴𝜑 } = { 𝑥 ∣ ( 𝑥𝐴𝜑 ) }
3 eqabcb ( { 𝑥 ∣ ( 𝑥𝐴𝜑 ) } = 𝐴 ↔ ∀ 𝑥 ( ( 𝑥𝐴𝜑 ) ↔ 𝑥𝐴 ) )
4 1 pm4.71i ( 𝑥𝐴 ↔ ( 𝑥𝐴𝜑 ) )
5 4 bicomi ( ( 𝑥𝐴𝜑 ) ↔ 𝑥𝐴 )
6 3 5 mpgbir { 𝑥 ∣ ( 𝑥𝐴𝜑 ) } = 𝐴
7 2 6 eqtri { 𝑥𝐴𝜑 } = 𝐴