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 )