Metamath Proof Explorer

Theorem ss2abim

Description: Class abstractions in a subclass relationship. Reverse direction of ss2ab which requires fewer axioms. (Contributed by SN, 2-Feb-2026)

Ref Expression
Assertion ss2abim ⊢ ∀ x φ → ψ → x | φ ⊆ x | ψ

Proof

Step Hyp Ref Expression
1 spsbim ⊢ ∀ x φ → ψ → y x φ → y x ψ
2 1 alrimiv ⊢ ∀ x φ → ψ → ∀ y y x φ → y x ψ
3 df-ss ⊢ x | φ ⊆ x | ψ ↔ ∀ y y ∈ x | φ → y ∈ x | ψ
4 df-clab ⊢ y ∈ x | φ ↔ y x φ
5 df-clab ⊢ y ∈ x | ψ ↔ y x ψ
6 4 5 imbi12i ⊢ y ∈ x | φ → y ∈ x | ψ ↔ y x φ → y x ψ
7 6 albii ⊢ ∀ y y ∈ x | φ → y ∈ x | ψ ↔ ∀ y y x φ → y x ψ
8 3 7 bitr2i ⊢ ∀ y y x φ → y x ψ ↔ x | φ ⊆ x | ψ
9 2 8 sylib ⊢ ∀ x φ → ψ → x | φ ⊆ x | ψ