Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Andrew Salmon
Set Theory
conss1
Next ⟩
ralbidar
Metamath Proof Explorer
Ascii
Structured
Theorem
conss1
Description:
Contrapositive law for subsets.
(Contributed by
Andrew Salmon
, 15-Jul-2011)
Ref
Expression
Assertion
conss1
⊢
( ( V ∖
𝐴
) ⊆
𝐵
↔ ( V ∖
𝐵
) ⊆
𝐴
)
Proof
Step
Hyp
Ref
Expression
1
difcom
⊢
( ( V ∖
𝐴
) ⊆
𝐵
↔ ( V ∖
𝐵
) ⊆
𝐴
)