Metamath Proof Explorer


Theorem relopabvOLD

Description: Obsolete version of relopab as of 26-Oct-2026. (Contributed by SN, 8-Sep-2024) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion relopabvOLD ⊢ Rel ⁡ x y | φ

Proof

Step Hyp Ref Expression
1 eqid ⊢ x y | φ = x y | φ
2 1 relopabiv ⊢ Rel ⁡ x y | φ