This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ss2ab

Description: Class abstractions in a subclass relationship. (Contributed by NM, 3-Jul-1994)

Ref Expression
Assertion ss2ab ⊢ x | φ ⊆ x | ψ ↔ ∀ x φ → ψ

Proof

Step Hyp Ref Expression
1 nfab1 ⊢ Ⅎ _ x x | φ
2 nfab1 ⊢ Ⅎ _ x x | ψ
3 1 2 dfssf ⊢ x | φ ⊆ x | ψ ↔ ∀ x x ∈ x | φ → x ∈ x | ψ
4 abid ⊢ x ∈ x | φ ↔ φ
5 abid ⊢ x ∈ x | ψ ↔ ψ
6 4 5 imbi12i ⊢ x ∈ x | φ → x ∈ x | ψ ↔ φ → ψ
7 6 albii ⊢ ∀ x x ∈ x | φ → x ∈ x | ψ ↔ ∀ x φ → ψ
8 3 7 bitri ⊢ x | φ ⊆ x | ψ ↔ ∀ x φ → ψ