# Metamath Proof Explorer

## Theorem pssdifcom2

Description: Two ways to express non-covering pairs of subsets. (Contributed by Stefan O'Rear, 31-Oct-2014)

Ref Expression
Assertion pssdifcom2 ${⊢}\left({A}\subseteq {C}\wedge {B}\subseteq {C}\right)\to \left({B}\subset {C}\setminus {A}↔{A}\subset {C}\setminus {B}\right)$

### Proof

Step Hyp Ref Expression
1 ssconb ${⊢}\left({B}\subseteq {C}\wedge {A}\subseteq {C}\right)\to \left({B}\subseteq {C}\setminus {A}↔{A}\subseteq {C}\setminus {B}\right)$
2 1 ancoms ${⊢}\left({A}\subseteq {C}\wedge {B}\subseteq {C}\right)\to \left({B}\subseteq {C}\setminus {A}↔{A}\subseteq {C}\setminus {B}\right)$
3 difcom ${⊢}{C}\setminus {A}\subseteq {B}↔{C}\setminus {B}\subseteq {A}$
4 3 notbii ${⊢}¬{C}\setminus {A}\subseteq {B}↔¬{C}\setminus {B}\subseteq {A}$
5 4 a1i ${⊢}\left({A}\subseteq {C}\wedge {B}\subseteq {C}\right)\to \left(¬{C}\setminus {A}\subseteq {B}↔¬{C}\setminus {B}\subseteq {A}\right)$
6 2 5 anbi12d ${⊢}\left({A}\subseteq {C}\wedge {B}\subseteq {C}\right)\to \left(\left({B}\subseteq {C}\setminus {A}\wedge ¬{C}\setminus {A}\subseteq {B}\right)↔\left({A}\subseteq {C}\setminus {B}\wedge ¬{C}\setminus {B}\subseteq {A}\right)\right)$
7 dfpss3 ${⊢}{B}\subset {C}\setminus {A}↔\left({B}\subseteq {C}\setminus {A}\wedge ¬{C}\setminus {A}\subseteq {B}\right)$
8 dfpss3 ${⊢}{A}\subset {C}\setminus {B}↔\left({A}\subseteq {C}\setminus {B}\wedge ¬{C}\setminus {B}\subseteq {A}\right)$
9 6 7 8 3bitr4g ${⊢}\left({A}\subseteq {C}\wedge {B}\subseteq {C}\right)\to \left({B}\subset {C}\setminus {A}↔{A}\subset {C}\setminus {B}\right)$