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

Metamath Proof Explorer

Theorem abssf

Description: Class abstraction in a subclass relationship. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypothesis abssf.1 ⊢ Ⅎ _ x A
Assertion abssf ⊢ x | φ ⊆ A ↔ ∀ x φ → x ∈ A

Proof

Step Hyp Ref Expression
1 abssf.1 ⊢ Ⅎ _ x A
2 1 abid2f ⊢ x | x ∈ A = A
3 2 sseq2i ⊢ x | φ ⊆ x | x ∈ A ↔ x | φ ⊆ A
4 ss2ab ⊢ x | φ ⊆ x | x ∈ A ↔ ∀ x φ → x ∈ A
5 3 4 bitr3i ⊢ x | φ ⊆ A ↔ ∀ x φ → x ∈ A