Metamath Proof Explorer


Syntax definition wiso

Description: Extend the definition of a wff to include the isomorphism property. Read: " H is an R , S isomorphism of A onto B ".

Ref Expression
Assertion wiso
wff H Isom R , S ( A , B )