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 A 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 questions are:
Are there other approaches for justification of "the isomorphism inference rule"?
Or maybe there are more simple expositions of Bourbaki approach?