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

Metamath Proof Explorer

Theorem reldisj

Description: Two ways of saying that two classes are disjoint, using the complement of B relative to a universe C . (Contributed by NM, 15-Feb-2007) (Proof shortened by Andrew Salmon, 26-Jun-2011) Avoid ax-12 . (Revised by GG, 28-Jun-2024)

Ref Expression
Assertion reldisj ( 𝐴 ⊆ 𝐶 → ( ( 𝐴 ∩ 𝐵 ) = ∅ ↔ 𝐴 ⊆ ( 𝐶 ∖ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 df-ss ⊢ ( 𝐴 ⊆ 𝐶 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶 ) )
2 eleq1w ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
3 eleq1w ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐶 ↔ 𝑦 ∈ 𝐶 ) )
4 2 3 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶 ) ↔ ( 𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐶 ) ) )
5 4 spw ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶 ) → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶 ) )
6 pm5.44 ⊢ ( ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶 ) → ( ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐵 ) ) ) )
7 eldif ⊢ ( 𝑥 ∈ ( 𝐶 ∖ 𝐵 ) ↔ ( 𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐵 ) )
8 7 imbi2i ⊢ ( ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ( 𝐶 ∖ 𝐵 ) ) ↔ ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐵 ) ) )
9 6 8 bitr4di ⊢ ( ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶 ) → ( ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ( 𝐶 ∖ 𝐵 ) ) ) )
10 5 9 syl ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶 ) → ( ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ( 𝐶 ∖ 𝐵 ) ) ) )
11 1 10 sylbi ⊢ ( 𝐴 ⊆ 𝐶 → ( ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ( 𝐶 ∖ 𝐵 ) ) ) )
12 11 albidv ⊢ ( 𝐴 ⊆ 𝐶 → ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ( 𝐶 ∖ 𝐵 ) ) ) )
13 disj1 ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵 ) )
14 df-ss ⊢ ( 𝐴 ⊆ ( 𝐶 ∖ 𝐵 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ( 𝐶 ∖ 𝐵 ) ) )
15 12 13 14 3bitr4g ⊢ ( 𝐴 ⊆ 𝐶 → ( ( 𝐴 ∩ 𝐵 ) = ∅ ↔ 𝐴 ⊆ ( 𝐶 ∖ 𝐵 ) ) )