Theorem pssdifcom1

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

	Ref	Expression
Assertion	pssdifcom1	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 ) → ( ( 𝐶 ∖ 𝐴 ) ⊊ 𝐵 ↔ ( 𝐶 ∖ 𝐵 ) ⊊ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		difcom	⊢ ( ( 𝐶 ∖ 𝐴 ) ⊆ 𝐵 ↔ ( 𝐶 ∖ 𝐵 ) ⊆ 𝐴 )
2	1	a1i	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 ) → ( ( 𝐶 ∖ 𝐴 ) ⊆ 𝐵 ↔ ( 𝐶 ∖ 𝐵 ) ⊆ 𝐴 ) )
3		ssconb	⊢ ( ( 𝐵 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐶 ) → ( 𝐵 ⊆ ( 𝐶 ∖ 𝐴 ) ↔ 𝐴 ⊆ ( 𝐶 ∖ 𝐵 ) ) )
4	3	ancoms	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 ) → ( 𝐵 ⊆ ( 𝐶 ∖ 𝐴 ) ↔ 𝐴 ⊆ ( 𝐶 ∖ 𝐵 ) ) )
5	4	notbid	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 ) → ( ¬ 𝐵 ⊆ ( 𝐶 ∖ 𝐴 ) ↔ ¬ 𝐴 ⊆ ( 𝐶 ∖ 𝐵 ) ) )
6	2 5	anbi12d	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 ) → ( ( ( 𝐶 ∖ 𝐴 ) ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ ( 𝐶 ∖ 𝐴 ) ) ↔ ( ( 𝐶 ∖ 𝐵 ) ⊆ 𝐴 ∧ ¬ 𝐴 ⊆ ( 𝐶 ∖ 𝐵 ) ) ) )
7		dfpss3	⊢ ( ( 𝐶 ∖ 𝐴 ) ⊊ 𝐵 ↔ ( ( 𝐶 ∖ 𝐴 ) ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ ( 𝐶 ∖ 𝐴 ) ) )
8		dfpss3	⊢ ( ( 𝐶 ∖ 𝐵 ) ⊊ 𝐴 ↔ ( ( 𝐶 ∖ 𝐵 ) ⊆ 𝐴 ∧ ¬ 𝐴 ⊆ ( 𝐶 ∖ 𝐵 ) ) )
9	6 7 8	3bitr4g	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 ) → ( ( 𝐶 ∖ 𝐴 ) ⊊ 𝐵 ↔ ( 𝐶 ∖ 𝐵 ) ⊊ 𝐴 ) )