Theorem idfudiag1lem

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

	Ref	Expression
Hypotheses	idfudiag1lem.1	|- ( ph -> ( _I |` A ) = ( A X. { B } ) )
	idfudiag1lem.2	|- ( ph -> A =/= (/) )
Assertion	idfudiag1lem	|- ( ph -> A = { B } )

Proof

Step	Hyp	Ref	Expression
1		idfudiag1lem.1	|- ( ph -> ( _I |` A ) = ( A X. { B } ) )
2		idfudiag1lem.2	|- ( ph -> A =/= (/) )
3		rnresi	|- ran ( _I |` A ) = A
4	1	rneqd	|- ( ph -> ran ( _I |` A ) = ran ( A X. { B } ) )
5	3 4	eqtr3id	|- ( ph -> A = ran ( A X. { B } ) )
6		rnxp	|- ( A =/= (/) -> ran ( A X. { B } ) = { B } )
7	2 6	syl	|- ( ph -> ran ( A X. { B } ) = { B } )
8	5 7	eqtrd	|- ( ph -> A = { B } )