Theorem iresn0n0

Description: The identity function restricted to a class A is empty iff the class A is empty. (Contributed by AV, 30-Jan-2024)

	Ref	Expression
Assertion	iresn0n0	$$⊢A=\varnothing \leftrightarrow {\mathrm{I}\upharpoonright }_A=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		opab0	$$⊢\left\{⟨x,y⟩|\left(x\in A\wedge y=x\right)\right\}=\varnothing \leftrightarrow \forall x\forall y\neg \left(x\in A\wedge y=x\right)$$
2		opabresid	$$⊢{\mathrm{I}\upharpoonright }_A=\left\{⟨x,y⟩|\left(x\in A\wedge y=x\right)\right\}$$
3	2	eqeq1i	$$⊢{\mathrm{I}\upharpoonright }_A=\varnothing \leftrightarrow \left\{⟨x,y⟩|\left(x\in A\wedge y=x\right)\right\}=\varnothing$$
4		nel02	$$⊢A=\varnothing \to \neg x\in A$$
5	4	intnanrd	$$⊢A=\varnothing \to \neg \left(x\in A\wedge y=x\right)$$
6	5	alrimivv	$$⊢A=\varnothing \to \forall x\forall y\neg \left(x\in A\wedge y=x\right)$$
7		ianor	$$⊢\neg \left(x\in A\wedge y=x\right)\leftrightarrow \left(\neg x\in A\vee \neg y=x\right)$$
8	7	albii	$$⊢\forall y\neg \left(x\in A\wedge y=x\right)\leftrightarrow \forall y\left(\neg x\in A\vee \neg y=x\right)$$
9		19.32v	$$⊢\forall y\left(\neg x\in A\vee \neg y=x\right)\leftrightarrow \left(\neg x\in A\vee \forall y\neg y=x\right)$$
10		id	$$⊢\neg x\in A\to \neg x\in A$$
11		ax6v	$$⊢\neg \forall y\neg y=x$$
12	11	pm2.21i	$$⊢\forall y\neg y=x\to \neg x\in A$$
13	10 12	jaoi	$$⊢\left(\neg x\in A\vee \forall y\neg y=x\right)\to \neg x\in A$$
14	9 13	sylbi	$$⊢\forall y\left(\neg x\in A\vee \neg y=x\right)\to \neg x\in A$$
15	8 14	sylbi	$$⊢\forall y\neg \left(x\in A\wedge y=x\right)\to \neg x\in A$$
16	15	alimi	$$⊢\forall x\forall y\neg \left(x\in A\wedge y=x\right)\to \forall x\neg x\in A$$
17		eq0	$$⊢A=\varnothing \leftrightarrow \forall x\neg x\in A$$
18	16 17	sylibr	$$⊢\forall x\forall y\neg \left(x\in A\wedge y=x\right)\to A=\varnothing$$
19	6 18	impbii	$$⊢A=\varnothing \leftrightarrow \forall x\forall y\neg \left(x\in A\wedge y=x\right)$$
20	1 3 19	3bitr4ri	$$⊢A=\varnothing \leftrightarrow {\mathrm{I}\upharpoonright }_A=\varnothing$$