| 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 401 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)) | |
| 2 | eldif 3961 | . . . 4 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)) | |
| 3 | 1, 2 | xchbinxr 335 | . . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ 𝑥 ∈ (𝐴 ∖ 𝐵)) |
| 4 | 3 | albii 1819 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵)) |
| 5 | df-ss 3968 | . 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
| 6 | eq0 4350 | . 2 ⊢ ((𝐴 ∖ 𝐵) = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵)) | |
| 7 | 4, 5, 6 | 3bitr4i 303 | 1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∖ 𝐵) = ∅) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∀wal 1538 = wceq 1540 ∈ wcel 2108 ∖ cdif 3948 ⊆ wss 3951 ∅c0 4333 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-dif 3954 df-ss 3968 df-nul 4334 |
| This theorem is referenced by: difn0 4367 pssdifn0 4368 difidALT 4377 vdif0 4469 difrab0eq 4470 difin0 4474 symdifv 5086 frpoind 6363 wfiOLD 6372 ordintdif 6434 dffv2 7004 fndifnfp 7196 tfi 7874 peano5 7915 frrlem13 8323 frrlem14 8324 wfrlem8OLD 8356 wfrlem16OLD 8364 tz7.49 8485 oe0m1 8559 sucdom2OLD 9122 sdomdif 9165 sucdom2 9243 php3 9249 php3OLD 9261 isinf 9296 isinfOLD 9297 unxpwdom2 9628 frind 9790 fin23lem26 10365 fin23lem21 10379 fin1a2lem13 10452 zornn0g 10545 fpwwe2lem12 10682 fpwwe2 10683 isumltss 15884 rpnnen2lem12 16261 symgsssg 19485 symgfisg 19486 psgnunilem5 19512 lspsnat 21147 lsppratlem6 21154 lspprat 21155 lbsextlem4 21163 cnsubrg 21445 opsrtoslem2 22080 psdmullem 22169 0ntr 23079 cmpfi 23416 dfconn2 23427 filconn 23891 cfinfil 23901 ufileu 23927 alexsublem 24052 ptcmplem2 24061 ptcmplem3 24062 restmetu 24583 reconnlem1 24848 bcthlem5 25362 itg10 25723 limcnlp 25913 noextendseq 27712 sltlpss 27945 upgrex 29109 uvtx01vtx 29414 ex-dif 30442 strlem1 32269 difininv 32536 eqdif 32538 difioo 32784 pmtrcnelor 33111 baselcarsg 34308 difelcarsg 34312 sibfof 34342 sitg0 34348 chtvalz 34644 onsucconni 36438 topdifinfeq 37351 nlpineqsn 37409 fdc 37752 setindtr 43036 oe0rif 43298 cantnfresb 43337 relnonrel 43600 inaex 44316 caragenunidm 46523 |
| Copyright terms: Public domain | W3C validator |