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	$$⊢\exists y\phi \to \left\{⟨x,y⟩|\phi \right\}\notin \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢x\in \mathrm{V}$$
2	1	biantrur	$$⊢\phi \leftrightarrow \left(x\in \mathrm{V}\wedge \phi \right)$$
3	2	opabbii	$$⊢\left\{⟨x,y⟩|\phi \right\}=\left\{⟨x,y⟩|\left(x\in \mathrm{V}\wedge \phi \right)\right\}$$
4	3	dmeqi	$$⊢\mathrm{dom}\left\{⟨x,y⟩|\phi \right\}=\mathrm{dom}\left\{⟨x,y⟩|\left(x\in \mathrm{V}\wedge \phi \right)\right\}$$
5		id	$$⊢\exists y\phi \to \exists y\phi$$
6	5	ralrimivw	$$⊢\exists y\phi \to \forall x\in \mathrm{V}\exists y\phi$$
7		dmopab3	$$⊢\forall x\in \mathrm{V}\exists y\phi \leftrightarrow \mathrm{dom}\left\{⟨x,y⟩|\left(x\in \mathrm{V}\wedge \phi \right)\right\}=\mathrm{V}$$
8	6 7	sylib	$$⊢\exists y\phi \to \mathrm{dom}\left\{⟨x,y⟩|\left(x\in \mathrm{V}\wedge \phi \right)\right\}=\mathrm{V}$$
9	4 8	syl5eq	$$⊢\exists y\phi \to \mathrm{dom}\left\{⟨x,y⟩|\phi \right\}=\mathrm{V}$$
10		vprc	$$⊢\neg \mathrm{V}\in \mathrm{V}$$
11	10	a1i	$$⊢\exists y\phi \to \neg \mathrm{V}\in \mathrm{V}$$
12	9 11	eqneltrd	$$⊢\exists y\phi \to \neg \mathrm{dom}\left\{⟨x,y⟩|\phi \right\}\in \mathrm{V}$$
13		dmexg	$$⊢\left\{⟨x,y⟩|\phi \right\}\in \mathrm{V}\to \mathrm{dom}\left\{⟨x,y⟩|\phi \right\}\in \mathrm{V}$$
14	12 13	nsyl	$$⊢\exists y\phi \to \neg \left\{⟨x,y⟩|\phi \right\}\in \mathrm{V}$$
15		df-nel	$$⊢\left\{⟨x,y⟩|\phi \right\}\notin \mathrm{V}\leftrightarrow \neg \left\{⟨x,y⟩|\phi \right\}\in \mathrm{V}$$
16	14 15	sylibr	$$⊢\exists y\phi \to \left\{⟨x,y⟩|\phi \right\}\notin \mathrm{V}$$