Syntax Definition wiso 5219

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-isom 5227 for more information.