Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Rodolfo Medina
Partitions
prtlem80
Next ⟩
brabsb2
Metamath Proof Explorer
Ascii
Unicode
Theorem
prtlem80
Description:
Lemma for
prter2
.
(Contributed by
Rodolfo Medina
, 17-Oct-2010)
Ref
Expression
Assertion
prtlem80
⊢
A
∈
B
→
¬
A
∈
C
∖
A
Proof
Step
Hyp
Ref
Expression
1
neldifsnd
⊢
A
∈
B
→
¬
A
∈
C
∖
A