Metamath Proof Explorer
Definition df-he
Description: The property of relation R being hereditary in class A .
(Contributed by RP, 27-Mar-2020)
|
|
Ref |
Expression |
|
Assertion |
df-he |
|
Detailed syntax breakdown
Step |
Hyp |
Ref |
Expression |
0 |
|
cR |
|
1 |
|
cA |
|
2 |
1 0
|
whe |
|
3 |
0 1
|
cima |
|
4 |
3 1
|
wss |
|
5 |
2 4
|
wb |
|