Metamath Proof Explorer


Theorem fvrcllb1d

Description: A set is a subset of its image under the reflexive closure. (Contributed by RP, 22-Jul-2020)

Ref Expression
Hypothesis fvrcllb1d.r φ R V
Assertion fvrcllb1d φ R r* R

Proof

Step Hyp Ref Expression
1 fvrcllb1d.r φ R V
2 dfrcl4 r* = r V n 0 1 r r n
3 prex 0 1 V
4 3 a1i φ 0 1 V
5 1ex 1 V
6 5 prid2 1 0 1
7 6 a1i φ 1 0 1
8 2 1 4 7 fvmptiunrelexplb1d φ R r* R