Description: Operation class abstraction expressed without existential quantifiers. (Contributed by NM, 16-Dec-2008)
Ref | Expression | ||
---|---|---|---|
Hypothesis | dfoprab3.1 | |
|
Assertion | dfoprab3 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfoprab3.1 | |
|
2 | dfoprab3s | |
|
3 | fvex | |
|
4 | fvex | |
|
5 | eqcom | |
|
6 | eqcom | |
|
7 | 5 6 | anbi12i | |
8 | eqopi | |
|
9 | 7 8 | sylan2b | |
10 | 9 1 | syl | |
11 | 10 | bicomd | |
12 | 11 | ex | |
13 | 3 4 12 | sbc2iedv | |
14 | 13 | pm5.32i | |
15 | 14 | opabbii | |
16 | 2 15 | eqtr2i | |