Metamath Proof Explorer


Syntax definition w-bnj13

Description: Extend wff notation with the following predicate: R is set-like on A . (New usage is discouraged.)

Ref Expression
Assertion w-bnj13 wff 𝑅 Se 𝐴