This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 ) → ( 𝐴 ⊆ ( 𝐶 ∖ 𝐵 ) ↔ 𝐵 ⊆ ( 𝐶 ∖ 𝐴 ) ) )