![]() |
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 403 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)) | |
2 | eldif 3925 | . . . 4 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)) | |
3 | 1, 2 | xchbinxr 335 | . . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ 𝑥 ∈ (𝐴 ∖ 𝐵)) |
4 | 3 | albii 1822 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵)) |
5 | dfss2 3935 | . 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
6 | eq0 4308 | . 2 ⊢ ((𝐴 ∖ 𝐵) = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵)) | |
7 | 4, 5, 6 | 3bitr4i 303 | 1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∖ 𝐵) = ∅) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 397 ∀wal 1540 = wceq 1542 ∈ wcel 2107 ∖ cdif 3912 ⊆ wss 3915 ∅c0 4287 |
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 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-v 3450 df-dif 3918 df-in 3922 df-ss 3932 df-nul 4288 |
This theorem is referenced by: difn0 4329 pssdifn0 4330 difidALT 4336 vdif0 4433 difrab0eq 4434 difin0 4438 symdifv 5051 frpoind 6301 wfiOLD 6310 ordintdif 6372 dffv2 6941 fndifnfp 7127 tfi 7794 peano5 7835 peano5OLD 7836 frrlem13 8234 frrlem14 8235 wfrlem8OLD 8267 wfrlem16OLD 8275 tz7.49 8396 oe0m1 8472 sucdom2OLD 9033 sdomdif 9076 sucdom2 9157 php3 9163 php3OLD 9175 isinf 9211 isinfOLD 9212 unxpwdom2 9531 frind 9693 fin23lem26 10268 fin23lem21 10282 fin1a2lem13 10355 zornn0g 10448 fpwwe2lem12 10585 fpwwe2 10586 isumltss 15740 rpnnen2lem12 16114 symgsssg 19256 symgfisg 19257 psgnunilem5 19283 lspsnat 20622 lsppratlem6 20629 lspprat 20630 lbsextlem4 20638 cnsubrg 20873 opsrtoslem2 21479 0ntr 22438 cmpfi 22775 dfconn2 22786 filconn 23250 cfinfil 23260 ufileu 23286 alexsublem 23411 ptcmplem2 23420 ptcmplem3 23421 restmetu 23942 reconnlem1 24205 bcthlem5 24708 itg10 25068 limcnlp 25258 noextendseq 27031 sltlpss 27258 upgrex 28085 uvtx01vtx 28387 ex-dif 29409 strlem1 31234 difininv 31486 eqdif 31488 difioo 31727 pmtrcnelor 31984 baselcarsg 32946 difelcarsg 32950 sibfof 32980 sitg0 32986 chtvalz 33282 onsucconni 34938 topdifinfeq 35850 nlpineqsn 35908 fdc 36233 setindtr 41377 oe0rif 41649 cantnfresb 41688 relnonrel 41933 inaex 42651 caragenunidm 44823 |
Copyright terms: Public domain | W3C validator |