Metamath Proof Explorer


Syntax definition wrelp

Description: Extend the definition of a wff to include the relation-preserving property. (Contributed by Eric Schmidt, 11-Oct-2025)

Ref Expression
Assertion wrelp wff 𝐻 RelPres 𝑅 , 𝑆 ( 𝐴 , 𝐵 )