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 3945 | . . . 4 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)) | |
3 | 1, 2 | xchbinxr 336 | . . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ 𝑥 ∈ (𝐴 ∖ 𝐵)) |
4 | 3 | albii 1811 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵)) |
5 | dfss2 3954 | . 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
6 | eq0 4307 | . 2 ⊢ ((𝐴 ∖ 𝐵) = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵)) | |
7 | 4, 5, 6 | 3bitr4i 304 | 1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∖ 𝐵) = ∅) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∧ wa 396 ∀wal 1526 = wceq 1528 ∈ wcel 2105 ∖ cdif 3932 ⊆ wss 3935 ∅c0 4290 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-v 3497 df-dif 3938 df-in 3942 df-ss 3951 df-nul 4291 |
This theorem is referenced by: difn0 4323 pssdifn0 4324 difid 4329 vdif0 4416 difrab0eq 4417 difin0 4420 symdifv 5000 wfi 6175 ordintdif 6234 dffv2 6750 fndifnfp 6931 tfi 7556 peano5 7593 wfrlem8 7953 wfrlem16 7961 tz7.49 8072 oe0m1 8137 sdomdif 8654 php3 8692 sucdom2 8703 isinf 8720 unxpwdom2 9041 fin23lem26 9736 fin23lem21 9750 fin1a2lem13 9823 zornn0g 9916 fpwwe2lem13 10053 fpwwe2 10054 isumltss 15193 rpnnen2lem12 15568 symgsssg 18526 symgfisg 18527 psgnunilem5 18553 lspsnat 19848 lsppratlem6 19855 lspprat 19856 lbsextlem4 19864 opsrtoslem2 20195 cnsubrg 20535 0ntr 21609 cmpfi 21946 dfconn2 21957 filconn 22421 cfinfil 22431 ufileu 22457 alexsublem 22582 ptcmplem2 22591 ptcmplem3 22592 restmetu 23109 reconnlem1 23363 bcthlem5 23860 itg10 24218 limcnlp 24405 upgrex 26805 uvtx01vtx 27107 ex-dif 28130 strlem1 29955 difininv 30207 eqdif 30209 difioo 30432 pmtrcnelor 30663 baselcarsg 31464 difelcarsg 31468 sibfof 31498 sitg0 31504 chtvalz 31800 frpoind 32978 frind 32983 frrlem13 33033 frrlem14 33034 noextendseq 33072 onsucconni 33683 topdifinfeq 34514 nlpineqsn 34572 fdc 34903 setindtr 39501 relnonrel 39827 inaex 40513 caragenunidm 42671 |
Copyright terms: Public domain | W3C validator |