Description: An ordered-pair class abstraction which does not depend on the first abstraction variable is a proper class. There must be, however, at least one set which satisfies the restricting wff. (Contributed by AV, 27-Dec-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | opabn1stprc | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex | |
|
2 | 1 | biantrur | |
3 | 2 | opabbii | |
4 | 3 | dmeqi | |
5 | id | |
|
6 | 5 | ralrimivw | |
7 | dmopab3 | |
|
8 | 6 7 | sylib | |
9 | 4 8 | eqtrid | |
10 | vprc | |
|
11 | 10 | a1i | |
12 | 9 11 | eqneltrd | |
13 | dmexg | |
|
14 | 12 13 | nsyl | |
15 | df-nel | |
|
16 | 14 15 | sylibr | |