Description: Implications for the value of an operation, defined by the maps-to notation with a class abstraction as a result, having an element. Here, the base set of the class abstraction depends on the first operand. Version of elovmporab1 with a disjoint variable condition, which does not require ax-13 . (Contributed by Alexander van der Vekens, 15-Jul-2018) (Revised by Gino Giotto, 26-Jan-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | elovmporab1w.o | |
|
elovmporab1w.v | |
||
Assertion | elovmporab1w | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elovmporab1w.o | |
|
2 | elovmporab1w.v | |
|
3 | 1 | elmpocl | |
4 | 1 | a1i | |
5 | csbeq1 | |
|
6 | 5 | ad2antrl | |
7 | sbceq1a | |
|
8 | sbceq1a | |
|
9 | 7 8 | sylan9bbr | |
10 | 9 | adantl | |
11 | 6 10 | rabeqbidv | |
12 | eqidd | |
|
13 | simpl | |
|
14 | simpr | |
|
15 | rabexg | |
|
16 | 2 15 | syl | |
17 | nfcv | |
|
18 | 17 | nfel1 | |
19 | nfcv | |
|
20 | 19 | nfel1 | |
21 | 18 20 | nfan | |
22 | nfcv | |
|
23 | 22 | nfel1 | |
24 | nfcv | |
|
25 | 24 | nfel1 | |
26 | 23 25 | nfan | |
27 | nfsbc1v | |
|
28 | nfcv | |
|
29 | 17 28 | nfcsbw | |
30 | 27 29 | nfrabw | |
31 | nfsbc1v | |
|
32 | 22 31 | nfsbcw | |
33 | nfcv | |
|
34 | 22 33 | nfcsbw | |
35 | 32 34 | nfrabw | |
36 | 4 11 12 13 14 16 21 26 22 19 30 35 | ovmpodxf | |
37 | 36 | eleq2d | |
38 | df-3an | |
|
39 | 38 | simplbi2com | |
40 | elrabi | |
|
41 | 39 40 | syl11 | |
42 | 37 41 | sylbid | |
43 | 3 42 | mpcom | |