Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ssdif0 | Structured version Visualization version GIF version |
Description: Subclass expressed in terms of difference. Exercise 7 of [TakeutiZaring] p. 22. (Contributed by NM, 29-Apr-1994.) |
Ref | Expression |
---|---|
ssdif0 | ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∖ 𝐵) = ∅) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iman 402 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)) | |
2 | eldif 3897 | . . . 4 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)) | |
3 | 1, 2 | xchbinxr 335 | . . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ 𝑥 ∈ (𝐴 ∖ 𝐵)) |
4 | 3 | albii 1822 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵)) |
5 | dfss2 3907 | . 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
6 | eq0 4277 | . 2 ⊢ ((𝐴 ∖ 𝐵) = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵)) | |
7 | 4, 5, 6 | 3bitr4i 303 | 1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∖ 𝐵) = ∅) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∀wal 1537 = wceq 1539 ∈ wcel 2106 ∖ cdif 3884 ⊆ wss 3887 ∅c0 4256 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1542 df-fal 1552 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-v 3434 df-dif 3890 df-in 3894 df-ss 3904 df-nul 4257 |
This theorem is referenced by: difn0 4298 pssdifn0 4299 difidALT 4305 vdif0 4402 difrab0eq 4403 difin0 4407 symdifv 5015 frpoind 6245 wfiOLD 6254 ordintdif 6315 dffv2 6863 fndifnfp 7048 tfi 7700 peano5 7740 peano5OLD 7741 frrlem13 8114 frrlem14 8115 wfrlem8OLD 8147 wfrlem16OLD 8155 tz7.49 8276 oe0m1 8351 sucdom2OLD 8869 sdomdif 8912 sucdom2 8989 php3 8995 php3OLD 9007 isinf 9036 unxpwdom2 9347 frind 9508 fin23lem26 10081 fin23lem21 10095 fin1a2lem13 10168 zornn0g 10261 fpwwe2lem12 10398 fpwwe2 10399 isumltss 15560 rpnnen2lem12 15934 symgsssg 19075 symgfisg 19076 psgnunilem5 19102 lspsnat 20407 lsppratlem6 20414 lspprat 20415 lbsextlem4 20423 cnsubrg 20658 opsrtoslem2 21263 0ntr 22222 cmpfi 22559 dfconn2 22570 filconn 23034 cfinfil 23044 ufileu 23070 alexsublem 23195 ptcmplem2 23204 ptcmplem3 23205 restmetu 23726 reconnlem1 23989 bcthlem5 24492 itg10 24852 limcnlp 25042 upgrex 27462 uvtx01vtx 27764 ex-dif 28787 strlem1 30612 difininv 30864 eqdif 30866 difioo 31103 pmtrcnelor 31360 baselcarsg 32273 difelcarsg 32277 sibfof 32307 sitg0 32313 chtvalz 32609 noextendseq 33870 sltlpss 34087 onsucconni 34626 topdifinfeq 35521 nlpineqsn 35579 fdc 35903 setindtr 40846 relnonrel 41195 inaex 41915 caragenunidm 44046 |
Copyright terms: Public domain | W3C validator |