Description: The notion " x is a subset of y " is absolute for transitive models. Compare Example I.16.3 of Kunen2 p. 96 and the following discussion. (Contributed by Eric Schmidt, 19-Oct-2025)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ssabso | |- ( ( Tr M /\ A e. M ) -> ( A C_ B <-> A. x e. M ( x e. A -> x e. B ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dfss3 | |- ( A C_ B <-> A. x e. A x e. B ) |
|
| 2 | ralabso | |- ( ( Tr M /\ A e. M ) -> ( A. x e. A x e. B <-> A. x e. M ( x e. A -> x e. B ) ) ) |
|
| 3 | 1 2 | bitrid | |- ( ( Tr M /\ A e. M ) -> ( A C_ B <-> A. x e. M ( x e. A -> x e. B ) ) ) |