Metamath Proof Explorer


Theorem opabn1stprc

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 yφxy|φV

Proof

Step Hyp Ref Expression
1 vex xV
2 1 biantrur φxVφ
3 2 opabbii xy|φ=xy|xVφ
4 3 dmeqi domxy|φ=domxy|xVφ
5 id yφyφ
6 5 ralrimivw yφxVyφ
7 dmopab3 xVyφdomxy|xVφ=V
8 6 7 sylib yφdomxy|xVφ=V
9 4 8 eqtrid yφdomxy|φ=V
10 vprc ¬VV
11 10 a1i yφ¬VV
12 9 11 eqneltrd yφ¬domxy|φV
13 dmexg xy|φVdomxy|φV
14 12 13 nsyl yφ¬xy|φV
15 df-nel xy|φV¬xy|φV
16 14 15 sylibr yφxy|φV