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 >. | ph }

Proof

Step Hyp Ref Expression
1 eqid 
 |-  { <. x , y >. | ph } = { <. x , y >. | ph }
2 1 relopabiv 
 |-  Rel { <. x , y >. | ph }