Theorem idfudiag1lem

Description: Lemma for idfudiag1bas and idfudiag1 . (Contributed by Zhi Wang, 19-Oct-2025)

	Ref	Expression
Hypotheses	idfudiag1lem.1	$$⊢\phi \to {\mathrm{I}\upharpoonright }_A=A\times \left\{B\right\}$$
	idfudiag1lem.2	$$⊢\phi \to A\ne \varnothing$$
Assertion	idfudiag1lem	$$⊢\phi \to A=\left\{B\right\}$$

Proof

Step	Hyp	Ref	Expression
1		idfudiag1lem.1	$$⊢\phi \to {\mathrm{I}\upharpoonright }_A=A\times \left\{B\right\}$$
2		idfudiag1lem.2	$$⊢\phi \to A\ne \varnothing$$
3		rnresi	$$⊢\mathrm{ran}\left({\mathrm{I}\upharpoonright }_A\right)=A$$
4	1	rneqd	$$⊢\phi \to \mathrm{ran}\left({\mathrm{I}\upharpoonright }_A\right)=\mathrm{ran}\left(A\times \left\{B\right\}\right)$$
5	3 4	eqtr3id	$$⊢\phi \to A=\mathrm{ran}\left(A\times \left\{B\right\}\right)$$
6		rnxp	$$⊢A\ne \varnothing \to \mathrm{ran}\left(A\times \left\{B\right\}\right)=\left\{B\right\}$$
7	2 6	syl	$$⊢\phi \to \mathrm{ran}\left(A\times \left\{B\right\}\right)=\left\{B\right\}$$
8	5 7	eqtrd	$$⊢\phi \to A=\left\{B\right\}$$