Metamath Proof Explorer
Description: A set is a subset of its image under the reflexive closure.
(Contributed by RP, 22-Jul-2020)
|
|
Ref |
Expression |
|
Hypothesis |
fvrcllb1d.r |
|
|
Assertion |
fvrcllb1d |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
fvrcllb1d.r |
|
2 |
|
dfrcl4 |
|
3 |
|
prex |
|
4 |
3
|
a1i |
|
5 |
|
1ex |
|
6 |
5
|
prid2 |
|
7 |
6
|
a1i |
|
8 |
2 1 4 7
|
fvmptiunrelexplb1d |
|