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