Step |
Hyp |
Ref |
Expression |
1 |
|
lpival.p |
|- P = ( LPIdeal ` R ) |
2 |
|
lpiss.u |
|- U = ( LIdeal ` R ) |
3 |
|
fveq2 |
|- ( r = R -> ( LIdeal ` r ) = ( LIdeal ` R ) ) |
4 |
|
fveq2 |
|- ( r = R -> ( LPIdeal ` r ) = ( LPIdeal ` R ) ) |
5 |
3 4
|
eqeq12d |
|- ( r = R -> ( ( LIdeal ` r ) = ( LPIdeal ` r ) <-> ( LIdeal ` R ) = ( LPIdeal ` R ) ) ) |
6 |
2 1
|
eqeq12i |
|- ( U = P <-> ( LIdeal ` R ) = ( LPIdeal ` R ) ) |
7 |
5 6
|
bitr4di |
|- ( r = R -> ( ( LIdeal ` r ) = ( LPIdeal ` r ) <-> U = P ) ) |
8 |
|
df-lpir |
|- LPIR = { r e. Ring | ( LIdeal ` r ) = ( LPIdeal ` r ) } |
9 |
7 8
|
elrab2 |
|- ( R e. LPIR <-> ( R e. Ring /\ U = P ) ) |