Theorem imasgimw

Description: A relabeling of the elements of a group induces an isomorphism to the relabeled group. This theorem is the same as imasgim but with an extra, unused, hypothesis B e. _V . We do this in anticipation of a revision to theorems about "s in which we use a sethood hypothesis to avoid ax-rep . When this happens, this theorem can be deleted and all usages replaced with usages of imasgim . (Contributed by Eric Schmidt, 24-Oct-2026)

	Ref	Expression
Hypotheses	imasgimw.u	|- ( ph -> U = ( F "s R ) )
	imasgimw.v	|- ( ph -> V = ( Base ` R ) )
	imasgimw.f	|- ( ph -> F : V -1-1-onto-> B )
	imasgimw.r	|- ( ph -> R e. Grp )
	imasgimw.b	|- B e. _V
Assertion	imasgimw	|- ( ph -> F e. ( R GrpIso U ) )

Proof

Step	Hyp	Ref	Expression
1		imasgimw.u	|- ( ph -> U = ( F "s R ) )
2		imasgimw.v	|- ( ph -> V = ( Base ` R ) )
3		imasgimw.f	|- ( ph -> F : V -1-1-onto-> B )
4		imasgimw.r	|- ( ph -> R e. Grp )
5		imasgimw.b	|- B e. _V
6	1 2 3 4	imasgim	|- ( ph -> F e. ( R GrpIso U ) )