In Internal Set Theory we can extend extensionality (set equivalence) via transfer. I'd like to work this out explicitly and then ask my question.
Extensionality: $\forall z(z\in x\iff z\in y)\implies x=y$
Transfer: Let $A(z,t_1,...,t_k)$ be an internal formula with free variables $z,t_1,...,t_k$ then,
$\forall^s t_1 ... \forall^s t_k (\forall^s z A\implies\forall z A)$
So in this case my $t$'s are $x$ and $y$ in the above formula. Let's do an example. Let $\nu$ be a nonstandard natural number and the notation $^SA$ is a standard set $\{a\in A | a\mbox{ is standard}\}$. Then $^S[0,\nu]$ and $\mathbb{N}$ contain the same standard elements, the standard natural numbers. So for any standard $n\in\phantom{ }^S[0,\nu]$ we are guaranteed $n\in\mathbb{N}$ and vice versa.
Here is my question. Am I then interpreting the implication in the Tranfer axiom correctly when I deduce, that for any element $x\in\phantom{ }^S[0,\nu]$ it is the case that $x\in\mathbb{N}$ and vice versa?
I'm not sure why it took me so long to fully grasp this idea. But yes, transferred extensionality implies that once two standard sets share the same standard elements they must share the same elements, standard or not.
So the set $^S[0,\nu]$ I reference above, really is the same as $\mathbb{N}$. Likewise for subset. For two standard sets A and B, $A\subset B$ as soon as for all standard $x\in A$ it is the case that $x\in B$.