Description: The subring predicate. (Contributed by Stefan O'Rear, 27-Nov-2014) (Proof shortened by AV, 12-Oct-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | issubrg.b | |
|
issubrg.i | |
||
Assertion | issubrg | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | issubrg.b | |
|
2 | issubrg.i | |
|
3 | df-subrg | |
|
4 | 3 | mptrcl | |
5 | simpll | |
|
6 | fveq2 | |
|
7 | 6 1 | eqtr4di | |
8 | 7 | pweqd | |
9 | oveq1 | |
|
10 | 9 | eleq1d | |
11 | fveq2 | |
|
12 | 11 2 | eqtr4di | |
13 | 12 | eleq1d | |
14 | 10 13 | anbi12d | |
15 | 8 14 | rabeqbidv | |
16 | 1 | fvexi | |
17 | 16 | pwex | |
18 | 17 | rabex | |
19 | 15 3 18 | fvmpt | |
20 | 19 | eleq2d | |
21 | oveq2 | |
|
22 | 21 | eleq1d | |
23 | eleq2 | |
|
24 | 22 23 | anbi12d | |
25 | 24 | elrab | |
26 | 16 | elpw2 | |
27 | 26 | anbi1i | |
28 | an12 | |
|
29 | 25 27 28 | 3bitri | |
30 | ibar | |
|
31 | 30 | anbi1d | |
32 | 29 31 | syl5bb | |
33 | 20 32 | bitrd | |
34 | 4 5 33 | pm5.21nii | |