Metamath Proof Explorer


Theorem ssabf

Description: Subclass of a class abstraction. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypothesis ssabf.1 𝑥 𝐴
Assertion ssabf ( 𝐴 ⊆ { 𝑥𝜑 } ↔ ∀ 𝑥 ( 𝑥𝐴𝜑 ) )

Proof

Step Hyp Ref Expression
1 ssabf.1 𝑥 𝐴
2 1 abid2f { 𝑥𝑥𝐴 } = 𝐴
3 2 sseq1i ( { 𝑥𝑥𝐴 } ⊆ { 𝑥𝜑 } ↔ 𝐴 ⊆ { 𝑥𝜑 } )
4 ss2ab ( { 𝑥𝑥𝐴 } ⊆ { 𝑥𝜑 } ↔ ∀ 𝑥 ( 𝑥𝐴𝜑 ) )
5 3 4 bitr3i ( 𝐴 ⊆ { 𝑥𝜑 } ↔ ∀ 𝑥 ( 𝑥𝐴𝜑 ) )