Say that "U" is the axiom that "For each set x, there exists a Grothendieck universe U such that x $\in$ U", where Grothendieck universes are defined in the usual way (or, if that's unclear, in this way). Also, say that "Ca" is the axiom that "For each cardinal κ, there is a strongly inaccessible cardinal $\lambda$ which is strictly larger than κ."

It's known that ZFC+U and ZFC+Ca are completely equivalent and prove the same sentences. A sentence is a theorem of ZFC+U iff it's a theorem of ZFC+Ca.

In addition to the above, there's also Tarski-Grothendieck set theory, which can be found here. The axioms of TG are

1. The axiom stating everything is a set
2. The axiom of extensionality from ZFC
3. The axiom of regularity from ZFC
4. The axiom of pairing from ZFC
5. The axiom of union from ZFC
6. The axiom schema of replacement from ZFC
7. Tarski's axiom A

Tarski's axiom A states that for any set $x$, there exists a set $y$ containing, $x$ itself, every subset of every member of $y$, the power set of every member of $y$, and every subset of $y$ of cardinality less than $y$.

These three axioms from ZFC are then implied as theorems of TG:

1. The axiom of infinity
2. The axiom of power set
3. The axiom schema of specification
4. The axiom of choice

My question is as follows: is TG also completely equivalent to ZFC+U and ZFC+Ca, equivalent in the same sense that something is a theorem of TG iff it's a theorem of the other two? Is TG just an axiomatization of ZFC+U/ZFC+Ca which removes redundant axioms and allows them to just be theorems? Or is there some subtle difference between TG and ZFC+U/ZFC+Ca, in that there's some sentence which TG proves that's undecidable in ZFC+U/ZFC+Ca or vice versa?

In other words, instead of typing ZFC+Grothendieck, can I just type TG and be referencing a different axiomatization of the exact same thing?

Say that "U" is the axiom that "For each set x, there exists a Grothendieck universe U such that x $\in$ U", where Grothendieck universes are defined in the usual way (or, if that's unclear, in this way). Also, say that "Ca" is the axiom that "For each cardinal κ, there is a strongly inaccessible cardinal $\lambda$ which is strictly larger than κ."

It's known that ZFC+U and ZFC+Ca are completely equivalent and prove the same sentences. A sentence is a theorem of ZFC+U iff it's a theorem of ZFC+Ca.

In addition to the above, there's also Tarski-Grothendieck set theory, which can be found here. The axioms of TG are

1. The axiom stating everything is a set
2. The axiom of extensionality from ZFC
3. The axiom of regularity from ZFC
4. The axiom of pairing from ZFC
5. The axiom of union from ZFC
6. The axiom schema of replacement from ZFC
7. Tarski's axiom A

Tarski's axiom A states that for any set $x$, there exists a set $y$ containing, $x$ itself, every subset of every member of $y$, the power set of every member of $y$, and every subset of $y$ of cardinality less than $y$.

These three axioms from ZFC are then implied as theorems of TG:

1. The axiom of infinity
2. The axiom of power set
3. The axiom schema of specification
4. The axiom of choice

My question is as follows: is TG also completely equivalent to ZFC+U and ZFC+Ca, equivalent in the same sense that something is a theorem of TG iff it's a theorem of the other two? Is TG just an axiomatization of ZFC+U/ZFC+Ca which removes redundant axioms and allows them to just be theorems? Or is there some subtle difference between TG and ZFC+U/ZFC+Ca, in that there's some sentence which TG proves that's undecidable in ZFC+U/ZFC+Ca or vice versa?

In other words, instead of typing ZFC+Grothendieck, can I just type TG and be referencing a different axiomatization of the exact same thing?

Say that "U" is the axiom that "For each set x, there exists a Grothendieck universe U such that x $\in$ U", where Grothendieck universes are defined in the usual way (or, if that's unclear, in this way). Also, say that "C" is the axiom that "For each cardinal κ, there is a strongly inaccessible cardinal $\lambda$ which is strictly larger than κ."

It's known that ZFC+U and ZFC+C are completely equivalent and prove the same sentences. A sentence is a theorem of ZFC+U iff it's a theorem of ZFC+C.

In addition to the above, there's also Tarski-Grothendieck set theory, which can be found here. The axioms of TG are

1. The axiom stating everything is a set
2. The axiom of extensionality from ZFC
3. The axiom of regularity from ZFC
4. The axiom of pairing from ZFC
5. The axiom of union from ZFC
6. The axiom schema of replacement from ZFC
7. Tarski's axiom A

Tarski's axiom A states that for any set $x$, there exists a set $y$ containing, $x$ itself, every subset of every member of $y$, the power set of every member of $y$, and every subset of $y$ of cardinality less than $y$.

These three axioms from ZFC are then implied as theorems of TG:

1. The axiom of infinity
2. The axiom of power set
3. The axiom schema of specification
4. The axiom of choice

My question is as follows: is TG also completely equivalent to ZFC+U and ZFC+C, equivalent in the same sense that something is a theorem of TG iff it's a theorem of the other two? Is TG just an axiomatization of ZFC+U/ZFC+C which removes redundant axioms and allows them to just be theorems? Or is there some subtle difference between TG and ZFC+U/ZFC+C, in that there's some sentence which TG proves that's undecidable in ZFC+U/ZFC+C or vice versa?

In other words, instead of typing ZFC+Grothendieck, can I just type TG and be referencing a different axiomatization of the exact same thing?

Say that "U" is the axiom that "For each set x, there exists a Grothendieck universe U such that x $\in$ U", where Grothendieck universes are defined in the usual way (or, if that's unclear, in this way). Also, say that "Ca" is the axiom that "For each cardinal κ, there is a strongly inaccessible cardinal $\lambda$ which is strictly larger than κ."

It's known that ZFC+U and ZFC+Ca are completely equivalent and prove the same sentences. A sentence is a theorem of ZFC+U iff it's a theorem of ZFC+Ca.

In addition to the above, there's also Tarski-Grothendieck set theory, which can be found here. The axioms of TG are

1. The axiom stating everything is a set
2. The axiom of extensionality from ZFC
3. The axiom of regularity from ZFC
4. The axiom of pairing from ZFC
5. The axiom of union from ZFC
6. The axiom schema of replacement from ZFC
7. Tarski's axiom A

Tarski's axiom A states that for any set $x$, there exists a set $y$ containing, $x$ itself, every subset of every member of $y$, the power set of every member of $y$, and every subset of $y$ of cardinality less than $y$.

These three axioms from ZFC are then implied as theorems of TG:

1. The axiom of infinity
2. The axiom of power set
3. The axiom schema of specification
4. The axiom of choice

My question is as follows: is TG also completely equivalent to ZFC+U and ZFC+Ca, equivalent in the same sense that something is a theorem of TG iff it's a theorem of the other two? Is TG just an axiomatization of ZFC+U/ZFC+Ca which removes redundant axioms and allows them to just be theorems? Or is there some subtle difference between TG and ZFC+U/ZFC+Ca, in that there's some sentence which TG proves that's undecidable in ZFC+U/ZFC+Ca or vice versa?

In other words, instead of typing ZFC+Grothendieck, can I just type TG and be referencing a different axiomatization of the exact same thing?