Metamath Proof Explorer


Syntax definition cdia

Description: Extend class notation with partial isomorphism A.

Ref Expression
Assertion cdia class DIsoA