Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Richard Penner
Propositions from _Begriffsschrift_
_Begriffsschrift_ Notation hints
idhe
Next ⟩
psshepw
Metamath Proof Explorer
Ascii
Unicode
Theorem
idhe
Description:
The identity relation is hereditary in any class.
(Contributed by
RP
, 28-Mar-2020)
Ref
Expression
Assertion
idhe
⊢
I
hereditary
A
Proof
Step
Hyp
Ref
Expression
1
idssxp
⊢
I
↾
A
⊆
A
×
A
2
dfhe2
⊢
I
hereditary
A
↔
I
↾
A
⊆
A
×
A
3
1
2
mpbir
⊢
I
hereditary
A