![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > reldisj | Structured version Visualization version GIF version |
Description: Two ways of saying that two classes are disjoint, using the complement of 𝐵 relative to a universe 𝐶. (Contributed by NM, 15-Feb-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
Ref | Expression |
---|---|
reldisj | ⊢ (𝐴 ⊆ 𝐶 → ((𝐴 ∩ 𝐵) = ∅ ↔ 𝐴 ⊆ (𝐶 ∖ 𝐵))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfss2 3740 | . . . 4 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)) | |
2 | pm5.44 532 | . . . . . 6 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) → ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐵)))) | |
3 | eldif 3733 | . . . . . . 7 ⊢ (𝑥 ∈ (𝐶 ∖ 𝐵) ↔ (𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐵)) | |
4 | 3 | imbi2i 325 | . . . . . 6 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐶 ∖ 𝐵)) ↔ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐵))) |
5 | 2, 4 | syl6bbr 278 | . . . . 5 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) → ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐶 ∖ 𝐵)))) |
6 | 5 | sps 2209 | . . . 4 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) → ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐶 ∖ 𝐵)))) |
7 | 1, 6 | sylbi 207 | . . 3 ⊢ (𝐴 ⊆ 𝐶 → ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐶 ∖ 𝐵)))) |
8 | 7 | albidv 2001 | . 2 ⊢ (𝐴 ⊆ 𝐶 → (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐶 ∖ 𝐵)))) |
9 | disj1 4162 | . 2 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵)) | |
10 | dfss2 3740 | . 2 ⊢ (𝐴 ⊆ (𝐶 ∖ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐶 ∖ 𝐵))) | |
11 | 8, 9, 10 | 3bitr4g 303 | 1 ⊢ (𝐴 ⊆ 𝐶 → ((𝐴 ∩ 𝐵) = ∅ ↔ 𝐴 ⊆ (𝐶 ∖ 𝐵))) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∧ wa 382 ∀wal 1629 = wceq 1631 ∈ wcel 2145 ∖ cdif 3720 ∩ cin 3722 ⊆ wss 3723 ∅c0 4063 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 837 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ral 3066 df-v 3353 df-dif 3726 df-in 3730 df-ss 3737 df-nul 4064 |
This theorem is referenced by: disj2 4168 ssdifsn 4454 oacomf1olem 7798 domdifsn 8199 elfiun 8492 cantnfp1lem3 8741 ssxr 10309 structcnvcnv 16078 fidomndrng 19522 elcls 21098 ist1-2 21372 nrmsep2 21381 nrmsep 21382 isnrm3 21384 isreg2 21402 hauscmplem 21430 connsub 21445 iunconnlem 21451 llycmpkgen2 21574 hausdiag 21669 trfil3 21912 isufil2 21932 filufint 21944 blcld 22530 i1fima2 23666 i1fd 23668 nbgrssvwo2 26481 nbgrssvwo2OLD 26484 pliguhgr 27680 poimirlem15 33757 itg2addnclem2 33794 ntrk0kbimka 38863 ntrneicls11 38914 gneispace 38958 |
Copyright terms: Public domain | W3C validator |