Syntax Definition wiso 4783

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