Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Glauco Siliprandi
Miscellanea
ssabf
Next ⟩
pssnssi
Metamath Proof Explorer
Ascii
Unicode
Theorem
ssabf
Description:
Subclass of a class abstraction.
(Contributed by
Glauco Siliprandi
, 26-Jun-2021)
Ref
Expression
Hypothesis
ssabf.1
⊢
Ⅎ
_
x
A
Assertion
ssabf
⊢
A
⊆
x
|
φ
↔
∀
x
x
∈
A
→
φ
Proof
Step
Hyp
Ref
Expression
1
ssabf.1
⊢
Ⅎ
_
x
A
2
1
abid2f
⊢
x
|
x
∈
A
=
A
3
2
sseq1i
⊢
x
|
x
∈
A
⊆
x
|
φ
↔
A
⊆
x
|
φ
4
ss2ab
⊢
x
|
x
∈
A
⊆
x
|
φ
↔
∀
x
x
∈
A
→
φ
5
3
4
bitr3i
⊢
A
⊆
x
|
φ
↔
∀
x
x
∈
A
→
φ