ax-ro-inst-2u - brismu bridi

	brismu bridi		< Previous Next > Nearby theorems
Mirrors > Home > Home > Th. List > ax-ro-inst-2u

Axiom ax-ro-inst-2u 242

Description: {ro bu'a} may be instantiated with any selbri. As example 13.3 of [CLL] p. 16 notes, this will be of limited use, and is included largely to allow for a second-order definition of equality.

**Hypotheses**
Ref	Expression
ax-ro-inst-2u.0	brirebla bo'a
ax-ro-inst-2u.1	⊢ ro bu'e zo'u ko'a bu'e

**Assertion**
Ref	Expression
ax-ro-inst-2u	⊢ ko'a bo'a

This axiom is referenced by: du-mintu 378

W3C validator