Syntax Definition wiso 2423

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

Hypotheses

Ref	Expression
cA	class A
cB	class B
cR	class R
cS	class S
cH	class H

Assertion

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

See definition df-iso 2439 for more information.

metamath.org