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 difference, union, and intersection of two classes The difference of two classes ssdif2d
Description: If A is contained in B and C is contained in D , then
( A \ D ) is contained in ( B \ C ) . Deduction form.
(Contributed by David Moews , 1-May-2017)
Ref
Expression
Hypotheses
ssdifd.1 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
ssdif2d.2 ⊢ ( 𝜑 → 𝐶 ⊆ 𝐷 )
Assertion
ssdif2d ⊢ ( 𝜑 → ( 𝐴 ∖ 𝐷 ) ⊆ ( 𝐵 ∖ 𝐶 ) )
Proof
Step
Hyp
Ref
Expression
1
ssdifd.1 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
2
ssdif2d.2 ⊢ ( 𝜑 → 𝐶 ⊆ 𝐷 )
3
2
sscond ⊢ ( 𝜑 → ( 𝐴 ∖ 𝐷 ) ⊆ ( 𝐴 ∖ 𝐶 ) )
4
1
ssdifd ⊢ ( 𝜑 → ( 𝐴 ∖ 𝐶 ) ⊆ ( 𝐵 ∖ 𝐶 ) )
5
3 4
sstrd ⊢ ( 𝜑 → ( 𝐴 ∖ 𝐷 ) ⊆ ( 𝐵 ∖ 𝐶 ) )