Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Steven Nguyen
Utility theorems
ssabdv
Next ⟩
sn-iotalem
Metamath Proof Explorer
Ascii
Unicode
Theorem
ssabdv
Description:
Deduction of abstraction subclass from implication.
(Contributed by
SN
, 22-Dec-2024)
Ref
Expression
Hypothesis
ssabdv.1
⊢
φ
→
x
∈
A
→
ψ
Assertion
ssabdv
⊢
φ
→
A
⊆
x
|
ψ
Proof
Step
Hyp
Ref
Expression
1
ssabdv.1
⊢
φ
→
x
∈
A
→
ψ
2
abid1
⊢
A
=
x
|
x
∈
A
3
1
ss2abdv
⊢
φ
→
x
|
x
∈
A
⊆
x
|
ψ
4
2
3
eqsstrid
⊢
φ
→
A
⊆
x
|
ψ