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

Proof

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