This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( E. y ph -> { <. x , y >. | ph } e/ _V )

Proof

Step Hyp Ref Expression
1 vex 
 |-  x e. _V
2 1 biantrur 
 |-  ( ph <-> ( x e. _V /\ ph ) )
3 2 opabbii 
 |-  { <. x , y >. | ph } = { <. x , y >. | ( x e. _V /\ ph ) }
4 3 dmeqi 
 |-  dom { <. x , y >. | ph } = dom { <. x , y >. | ( x e. _V /\ ph ) }
5 id 
 |-  ( E. y ph -> E. y ph )
6 5 ralrimivw 
 |-  ( E. y ph -> A. x e. _V E. y ph )
7 dmopab3 
 |-  ( A. x e. _V E. y ph <-> dom { <. x , y >. | ( x e. _V /\ ph ) } = _V )
8 6 7 sylib 
 |-  ( E. y ph -> dom { <. x , y >. | ( x e. _V /\ ph ) } = _V )
9 4 8 eqtrid 
 |-  ( E. y ph -> dom { <. x , y >. | ph } = _V )
10 vprc 
 |-  -. _V e. _V
11 10 a1i 
 |-  ( E. y ph -> -. _V e. _V )
12 9 11 eqneltrd 
 |-  ( E. y ph -> -. dom { <. x , y >. | ph } e. _V )
13 dmexg 
 |-  ( { <. x , y >. | ph } e. _V -> dom { <. x , y >. | ph } e. _V )
14 12 13 nsyl 
 |-  ( E. y ph -> -. { <. x , y >. | ph } e. _V )
15 df-nel 
 |-  ( { <. x , y >. | ph } e/ _V <-> -. { <. x , y >. | ph } e. _V )
16 14 15 sylibr 
 |-  ( E. y ph -> { <. x , y >. | ph } e/ _V )