Metamath Proof Explorer


Syntax definition whe

Description: The property of relation R being hereditary in class A .

Ref Expression
Assertion whe wff 𝑅 hereditary 𝐴