So, as you've noticed, this notion is absolutely ubiquitous.
There's a general notion of "isomorphic objects are equal (for all intents and purposes)". Particularly for categorists, notions that distinguish between isomorphic (or more generally, equivalent) objects are often referred to as "evil". In category theory, the principle you describe is called the principle of equivalence (or principle of isomorphism for a weaker notion). Most definitions of category theory use standard set theory and thus readily allow for evil definitions. As such, there is no principle of equivalence for those definitions; you can readily state properties that do not hold under equivalence of categories (or even isomorphisms of categories). This is because, in standard set theory, there is a global notion of equality which will always be able to distinguish between non-equal isomorphic objects.
If you look at the link above, you'll notice a lot of references to Homotopy Type Theory. This is a very new and very exciting development that directly addresses this issue. The most relevant part for you is the Univalence Axiom. The Univalence Axiom literally states that, in the context of homotopy type theory, equality is equivalent to equivalence. So all that treating isomorphic objects as equal is completely justified in homotopy type theory. By itself that wouldn't be that exciting, but homotopy type theory is a (fairly minor in some ways) extension of Martin Löf type theory which has been studied by type theorists and computer scientists and implemented for decades. It is the logical foundation for the Coq proof assistant. This means that 1) we have implementations of this logic already, 2) this logic is demonstrably able to formalize just about any mathematical notion, and 3) people are already doing real math in this. In other words, this incarnation of the principle of equivalence effectively encompasses all of mathematics (in practice), and homotopy type theory provides a possible "foundations" for mathematics that much more directly matches how mathematicians actually do mathematics.
There are other approaches to this besides homotopy type theory. The link above mentioned FOLDS which is a much more conservative approach, but Makkai's work is generally worth checking out.
To step back a bit, the reason there is no theorem like you mention in category theory (as should be clear from the above) is that it isn't a theorem about category theory. It's a theorem about whatever meta-logic you are using to define category theory and those predicates $P$. There are three routes to go from here. You can just give up on such a property which is, technically, what just about everyone does for category theory. You can formulate a logic that is easy to specify and for which well-formedness is easy to check, and then prove the property about this logic. This is essentially what happens at the informal level and occasionally is formalized. For example, you can easily prove that the theorems in Peano arithmetic do not depend on what exactly numbers are, or that rational number arithmetic is well-defined. The problem with this route is that it is restrictive; only relatively simple properties can be stated and oftentimes even then only awkwardly. The third route, then, is to make a rich (but difficult to fully specify) logic that allows you to naturally and directly express what you want but whose well-formedness is (relatively) difficult to verify. This is the route homotopy type theory takes. (FOLDS is in between the second and third route.) This is what roughly what happens at an informal level for most mathematical work. Nominally set theory is the logic we're working in, but it is understood that polite company does not ask whether $2\in 3$ or whether $A\times B \times C$ is $(A\times B)\times C$ or $A\times(B\times C)$ or something else. There's an implicit notion of/language for "reasonable" questions to ask, and for those "reasonable" questions isomorphic objects are not distinguished.