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

Proof

Step Hyp Ref Expression
1 rabeqcOLD.1 xAφ
2 df-rab xA|φ=x|xAφ
3 eqabcb x|xAφ=AxxAφxA
4 1 pm4.71i xAxAφ
5 4 bicomi xAφxA
6 3 5 mpgbir x|xAφ=A
7 2 6 eqtri xA|φ=A