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	$$⊢\phi \to U=F{“}_{𝑠}R$$
	imasgimw.v	$$⊢\phi \to V={\mathrm{Base}}_R$$
	imasgimw.f	$$⊢\phi \to F:V\underset{1-1\; onto}{⟶}B$$
	imasgimw.r	$$⊢\phi \to R\in \mathrm{Grp}$$
	imasgimw.b	$$⊢B\in \mathrm{V}$$
Assertion	imasgimw	$$⊢\phi \to F\in \left(R\mathrm{GrpIso}U\right)$$

Proof

Step	Hyp	Ref	Expression
1		imasgimw.u	$$⊢\phi \to U=F{“}_{𝑠}R$$
2		imasgimw.v	$$⊢\phi \to V={\mathrm{Base}}_R$$
3		imasgimw.f	$$⊢\phi \to F:V\underset{1-1\; onto}{⟶}B$$
4		imasgimw.r	$$⊢\phi \to R\in \mathrm{Grp}$$
5		imasgimw.b	$$⊢B\in \mathrm{V}$$
6	1 2 3 4	imasgim	$$⊢\phi \to F\in \left(R\mathrm{GrpIso}U\right)$$