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
Metamath Proof Explorer
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
⊢ ( 𝜑 → ( 𝐴 ∖ 𝐷 ) ⊆ ( 𝐵 ∖ 𝐶 ) )