This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - start with the Axiom of Extensionality The empty set ssdifin0
Description: A subset of a difference does not intersect the subtrahend. (Contributed by Jeff Hankins , 1-Sep-2013) (Proof shortened by Mario Carneiro , 24-Aug-2015)
Ref
Expression
Assertion
ssdifin0 ⊢ ( 𝐴 ⊆ ( 𝐵 ∖ 𝐶 ) → ( 𝐴 ∩ 𝐶 ) = ∅ )
Proof
Step
Hyp
Ref
Expression
1
ssrin ⊢ ( 𝐴 ⊆ ( 𝐵 ∖ 𝐶 ) → ( 𝐴 ∩ 𝐶 ) ⊆ ( ( 𝐵 ∖ 𝐶 ) ∩ 𝐶 ) )
2
disjdifr ⊢ ( ( 𝐵 ∖ 𝐶 ) ∩ 𝐶 ) = ∅
3
sseq0 ⊢ ( ( ( 𝐴 ∩ 𝐶 ) ⊆ ( ( 𝐵 ∖ 𝐶 ) ∩ 𝐶 ) ∧ ( ( 𝐵 ∖ 𝐶 ) ∩ 𝐶 ) = ∅ ) → ( 𝐴 ∩ 𝐶 ) = ∅ )
4
1 2 3
sylancl ⊢ ( 𝐴 ⊆ ( 𝐵 ∖ 𝐶 ) → ( 𝐴 ∩ 𝐶 ) = ∅ )