df-pamei - brismu bridi

	brismu bridi		< Previous Next > Nearby theorems
Mirrors > Home > Home > Th. List > df-pamei

Definition df-pamei 253

Description: The singleton set is the unique set whose elements are all isomorphic. Since we use the full semantics of second-order logic, we cannot construct the witness isomorphisms. As a compromise, we construct the isomorphism between any two elements of any particular singleton set.

**Assertion**
Ref	Expression
df-pamei	⊢ go ko'a pamei ko'e .e ko'i gi ko'e du ko'i

This definition is referenced by: pameii 254

W3C validator