This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 )