Description: A set is a subset of its image under the identity relation. (Contributed by RP, 22-Jul-2020) (Proof modification is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypothesis | fvilbdRP.r | |- ( ph -> R e. _V ) |
|
Assertion | fvilbdRP | |- ( ph -> R C_ ( _I ` R ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fvilbdRP.r | |- ( ph -> R e. _V ) |
|
2 | dfid6 | |- _I = ( r e. _V |-> U_ n e. { 1 } ( r ^r n ) ) |
|
3 | snex | |- { 1 } e. _V |
|
4 | 3 | a1i | |- ( ph -> { 1 } e. _V ) |
5 | 1ex | |- 1 e. _V |
|
6 | 5 | snid | |- 1 e. { 1 } |
7 | 6 | a1i | |- ( ph -> 1 e. { 1 } ) |
8 | 2 1 4 7 | fvmptiunrelexplb1d | |- ( ph -> R C_ ( _I ` R ) ) |