I'm looking for a strict book/pdf about logic which discusses formal systems in great detail. I only know basic stuff. It should cover:
definitions (like $(\exists x \varphi\leftrightarrow\lnot\forall x\lnot\varphi))$ inside the formal system (what to take care of when making definitions in a formal system)
distinct variables (and that we can make a formal system without the concept of "free" variables)
substitutions (would be nice if most would be taken care of "inside" the formal system)
using classes in zfc in a way, that they can always be eliminated (with proof)
defining ordinal addition etc. "inside" the formal system and working with the definition "inside" the formal system.
I shall suggest the resources linked from here. In particular since you seem to know basic logic, you probably should go straight to Stephen Simpson's notes. As for your desire to use classes in ZFC in a way that can be eliminated, you can rigorously manipulate definable classes and class functions by adding definitorial expansion to ZFC, because it is conservative and can be eliminated, which any proper logic textbook should mention (such as Rautenberg's in my first link). I think my second link should also address your question about ordinals; they form a definable class over ZFC and hence you can formally reason about them via definitorial expansion.