Metamath Proof Explorer

Theorem ssabso

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 ∈ M → A ⊆ B ↔ ∀ x ∈ M x ∈ A → x ∈ B

Proof

Step Hyp Ref Expression
1 dfss3 ⊢ A ⊆ B ↔ ∀ x ∈ A x ∈ B
2 ralabso ⊢ Tr ⁡ M ∧ A ∈ M → ∀ x ∈ A x ∈ B ↔ ∀ x ∈ M x ∈ A → x ∈ B
3 1 2 bitrid ⊢ Tr ⁡ M ∧ A ∈ M → A ⊆ B ↔ ∀ x ∈ M x ∈ A → x ∈ B