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	⊢ ( 𝜑 → 𝑈 = ( 𝐹 “s 𝑅 ) )
	imasgimw.v	⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
	imasgimw.f	⊢ ( 𝜑 → 𝐹 : 𝑉 ⟶1-1onto 𝐵 )
	imasgimw.r	⊢ ( 𝜑 → 𝑅 ∈ Grp )
	imasgimw.b	⊢ 𝐵 ∈ V
Assertion	imasgimw	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑅 GrpIso 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		imasgimw.u	⊢ ( 𝜑 → 𝑈 = ( 𝐹 “s 𝑅 ) )
2		imasgimw.v	⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
3		imasgimw.f	⊢ ( 𝜑 → 𝐹 : 𝑉 ⟶1-1onto 𝐵 )
4		imasgimw.r	⊢ ( 𝜑 → 𝑅 ∈ Grp )
5		imasgimw.b	⊢ 𝐵 ∈ V
6	1 2 3 4	imasgim	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑅 GrpIso 𝑈 ) )