Let me give an example:

- this is a definition in object language: R(x,y) is a symmetric formula ↔ （∀x∀y(R(x,y)→R(y,x))）

2.this is a definition in metatheory: R(x,y) is a symmetric formula if and only if R(x,y)→R(y,x) is a theorem. In other words: R(x,y) is a symmetric formula if and only if ⊢ R(x,y)→R(y,x). In other words: R(x,y) is a symmetric formula if and only if ⊢∀x∀y(R(x,y)→R(y,x))

I have the following questions: 1. These two definitions seem to imply all of theorems of object theory can be described in metatheory,Is that so ? How to precise state and prove this translation process for every theorem?

2.Our everyday reasoning in mathematics , in the end is in the object language or in the meta-language ?

another example:

I have seen a paragraph of text:

Thus, in the metatheory “P : A → A is an equivalence relation” means that “P ⊆ A × A and P is reflexive, symmetric, and transitive” is true, whereas in ZFC it means that the quoted (quasi) translation is provable (or has been taken as an assumption).

I consider the following words is another definition: ⊢ [(P : A → A is an equivalence relation)↔(P ⊆ A × A and The translations of the reflexive, symmetric, and transitive properties in the formal language)].

I want to know the difference between these two statements.