Suppose we are writing very detailed proofs, absolutely without any gaps (for example, for checking proofs by computer).

In such formal proofs every step (even a trivial one) must be justified.

For example, when we have proved that A = B and A is a prime number, we can infer that B is also a prime number.

We can justify this step by Leibniz Law (which may be represented by an axiom of Predicate Calculus with Equality).

When a group A is isomorphic to a group B and the group G is simple, then we can infer that the group B is also simple.

We can say , that "the isomorphism inference rule" was used in that case.

To justify such inferences, Bourbaki developed a general theory of isomorphism (see their book "Theory of Sets").

Because the Bourbaki theory is rather complicated, my question is:

Are there other approaches for justification of "the isomorphism inference rule".

Or maybe there are more simple expositions of Bourbaki approach?