![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dfss4 | Structured version Visualization version GIF version |
Description: Subclass defined in terms of class difference. See comments under dfun2 4275. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
Ref | Expression |
---|---|
dfss4 | ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝐴)) = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sseqin2 4230 | . 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∩ 𝐴) = 𝐴) | |
2 | eldif 3972 | . . . . . . 7 ⊢ (𝑥 ∈ (𝐵 ∖ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴)) | |
3 | 2 | notbii 320 | . . . . . 6 ⊢ (¬ 𝑥 ∈ (𝐵 ∖ 𝐴) ↔ ¬ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴)) |
4 | 3 | anbi2i 623 | . . . . 5 ⊢ ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ (𝐵 ∖ 𝐴)) ↔ (𝑥 ∈ 𝐵 ∧ ¬ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴))) |
5 | elin 3978 | . . . . . 6 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴)) | |
6 | abai 827 | . . . . . 6 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴))) | |
7 | iman 401 | . . . . . . 7 ⊢ ((𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴) ↔ ¬ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴)) | |
8 | 7 | anbi2i 623 | . . . . . 6 ⊢ ((𝑥 ∈ 𝐵 ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)) ↔ (𝑥 ∈ 𝐵 ∧ ¬ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴))) |
9 | 5, 6, 8 | 3bitri 297 | . . . . 5 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ¬ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴))) |
10 | 4, 9 | bitr4i 278 | . . . 4 ⊢ ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ (𝐵 ∖ 𝐴)) ↔ 𝑥 ∈ (𝐵 ∩ 𝐴)) |
11 | 10 | difeqri 4137 | . . 3 ⊢ (𝐵 ∖ (𝐵 ∖ 𝐴)) = (𝐵 ∩ 𝐴) |
12 | 11 | eqeq1i 2739 | . 2 ⊢ ((𝐵 ∖ (𝐵 ∖ 𝐴)) = 𝐴 ↔ (𝐵 ∩ 𝐴) = 𝐴) |
13 | 1, 12 | bitr4i 278 | 1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝐴)) = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1536 ∈ wcel 2105 ∖ cdif 3959 ∩ cin 3961 ⊆ wss 3962 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-ext 2705 |
This theorem depends on definitions: df-bi 207 df-an 396 df-3an 1088 df-tru 1539 df-ex 1776 df-sb 2062 df-clab 2712 df-cleq 2726 df-clel 2813 df-rab 3433 df-v 3479 df-dif 3965 df-in 3969 df-ss 3979 |
This theorem is referenced by: ssdifim 4278 dfin4 4283 sscon34b 4309 sorpsscmpl 7752 sbthlem3 9123 fin23lem7 10353 fin23lem11 10354 compsscnvlem 10407 compssiso 10411 isf34lem4 10414 efgmnvl 19746 frlmlbs 21834 isopn2 23055 iincld 23062 iuncld 23068 clsval2 23073 ntrval2 23074 ntrdif 23075 clsdif 23076 cmclsopn 23085 opncldf1 23107 indiscld 23114 mretopd 23115 restcld 23195 pnrmopn 23366 conndisj 23439 hausllycmp 23517 kqcldsat 23756 filufint 23943 cfinufil 23951 ufilen 23953 alexsublem 24067 bcth3 25378 inmbl 25590 iccmbl 25614 mbfimaicc 25679 i1fd 25729 itgss3 25864 difuncomp 32573 iundifdifd 32581 iundifdif 32582 supppreima 32705 pmtrcnelor 33093 ist0cld 33793 cldssbrsiga 34167 unelcarsg 34293 kur14lem4 35193 cldbnd 36308 clsun 36310 mblfinlem3 37645 mblfinlem4 37646 ismblfin 37647 itg2addnclem 37657 fdc 37731 dssmapnvod 44009 ntrclsfveq1 44049 ntrclsfveq 44051 ntrclsneine0lem 44053 ntrclsiso 44056 ntrclsk2 44057 ntrclskb 44058 ntrclsk3 44059 ntrclsk13 44060 ntrclsk4 44061 clsneiel2 44098 neicvgel2 44109 salincl 46279 salexct 46289 ovnsubadd2lem 46600 lincext2 48300 opncldeqv 48697 |
Copyright terms: Public domain | W3C validator |