Theorem ssconb

Description: Contraposition law for subsets. (Contributed by NM, 22-Mar-1998)

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

Proof

Step	Hyp	Ref	Expression
1		ssel	⊢ ( 𝐴 ⊆ 𝐶 → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶 ) )
2		ssel	⊢ ( 𝐵 ⊆ 𝐶 → ( 𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶 ) )
3		pm5.1	⊢ ( ( ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶 ) ∧ ( 𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶 ) ) → ( ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶 ) ↔ ( 𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶 ) ) )
4	1 2 3	syl2an	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 ) → ( ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶 ) ↔ ( 𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶 ) ) )
5		con2b	⊢ ( ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵 ) ↔ ( 𝑥 ∈ 𝐵 → ¬ 𝑥 ∈ 𝐴 ) )
6	5	a1i	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 ) → ( ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵 ) ↔ ( 𝑥 ∈ 𝐵 → ¬ 𝑥 ∈ 𝐴 ) ) )
7	4 6	anbi12d	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 ) → ( ( ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶 ) ∧ ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵 ) ) ↔ ( ( 𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶 ) ∧ ( 𝑥 ∈ 𝐵 → ¬ 𝑥 ∈ 𝐴 ) ) ) )
8		jcab	⊢ ( ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐵 ) ) ↔ ( ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶 ) ∧ ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵 ) ) )
9		jcab	⊢ ( ( 𝑥 ∈ 𝐵 → ( 𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐴 ) ) ↔ ( ( 𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶 ) ∧ ( 𝑥 ∈ 𝐵 → ¬ 𝑥 ∈ 𝐴 ) ) )
10	7 8 9	3bitr4g	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 ) → ( ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐵 ) ) ↔ ( 𝑥 ∈ 𝐵 → ( 𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐴 ) ) ) )
11		eldif	⊢ ( 𝑥 ∈ ( 𝐶 ∖ 𝐵 ) ↔ ( 𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐵 ) )
12	11	imbi2i	⊢ ( ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ( 𝐶 ∖ 𝐵 ) ) ↔ ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐵 ) ) )
13		eldif	⊢ ( 𝑥 ∈ ( 𝐶 ∖ 𝐴 ) ↔ ( 𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐴 ) )
14	13	imbi2i	⊢ ( ( 𝑥 ∈ 𝐵 → 𝑥 ∈ ( 𝐶 ∖ 𝐴 ) ) ↔ ( 𝑥 ∈ 𝐵 → ( 𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐴 ) ) )
15	10 12 14	3bitr4g	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 ) → ( ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ( 𝐶 ∖ 𝐵 ) ) ↔ ( 𝑥 ∈ 𝐵 → 𝑥 ∈ ( 𝐶 ∖ 𝐴 ) ) ) )
16	15	albidv	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 ) → ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ( 𝐶 ∖ 𝐵 ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → 𝑥 ∈ ( 𝐶 ∖ 𝐴 ) ) ) )
17		df-ss	⊢ ( 𝐴 ⊆ ( 𝐶 ∖ 𝐵 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ( 𝐶 ∖ 𝐵 ) ) )
18		df-ss	⊢ ( 𝐵 ⊆ ( 𝐶 ∖ 𝐴 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → 𝑥 ∈ ( 𝐶 ∖ 𝐴 ) ) )
19	16 17 18	3bitr4g	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 ) → ( 𝐴 ⊆ ( 𝐶 ∖ 𝐵 ) ↔ 𝐵 ⊆ ( 𝐶 ∖ 𝐴 ) ) )