Metamath Proof Explorer


Syntax definition wprt

Description: Extend the definition of a wff to include the partition predicate.

Ref Expression
Assertion wprt wff Prt A