![]() |
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 4162. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
Ref | Expression |
---|---|
dfss4 | ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝐴)) = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sseqin2 4118 | . 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∩ 𝐴) = 𝐴) | |
2 | eldif 3875 | . . . . . . 7 ⊢ (𝑥 ∈ (𝐵 ∖ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴)) | |
3 | 2 | notbii 321 | . . . . . 6 ⊢ (¬ 𝑥 ∈ (𝐵 ∖ 𝐴) ↔ ¬ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴)) |
4 | 3 | anbi2i 622 | . . . . 5 ⊢ ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ (𝐵 ∖ 𝐴)) ↔ (𝑥 ∈ 𝐵 ∧ ¬ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴))) |
5 | elin 4096 | . . . . . 6 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴)) | |
6 | abai 824 | . . . . . 6 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴))) | |
7 | iman 402 | . . . . . . 7 ⊢ ((𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴) ↔ ¬ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴)) | |
8 | 7 | anbi2i 622 | . . . . . 6 ⊢ ((𝑥 ∈ 𝐵 ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)) ↔ (𝑥 ∈ 𝐵 ∧ ¬ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴))) |
9 | 5, 6, 8 | 3bitri 298 | . . . . 5 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ¬ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴))) |
10 | 4, 9 | bitr4i 279 | . . . 4 ⊢ ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ (𝐵 ∖ 𝐴)) ↔ 𝑥 ∈ (𝐵 ∩ 𝐴)) |
11 | 10 | difeqri 4028 | . . 3 ⊢ (𝐵 ∖ (𝐵 ∖ 𝐴)) = (𝐵 ∩ 𝐴) |
12 | 11 | eqeq1i 2802 | . 2 ⊢ ((𝐵 ∖ (𝐵 ∖ 𝐴)) = 𝐴 ↔ (𝐵 ∩ 𝐴) = 𝐴) |
13 | 1, 12 | bitr4i 279 | 1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝐴)) = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∧ wa 396 = wceq 1525 ∈ wcel 2083 ∖ cdif 3862 ∩ cin 3864 ⊆ wss 3865 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 ax-6 1951 ax-7 1996 ax-8 2085 ax-9 2093 ax-10 2114 ax-11 2128 ax-12 2143 ax-ext 2771 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-tru 1528 df-ex 1766 df-nf 1770 df-sb 2045 df-clab 2778 df-cleq 2790 df-clel 2865 df-nfc 2937 df-v 3442 df-dif 3868 df-in 3872 df-ss 3880 |
This theorem is referenced by: ssdifim 4165 dfin4 4170 sorpsscmpl 7325 sbthlem3 8483 fin23lem7 9591 fin23lem11 9592 compsscnvlem 9645 compssiso 9649 isf34lem4 9652 efgmnvl 18571 frlmlbs 20627 isopn2 21328 iincld 21335 iuncld 21341 clsval2 21346 ntrval2 21347 ntrdif 21348 clsdif 21349 cmclsopn 21358 opncldf1 21380 indiscld 21387 mretopd 21388 restcld 21468 pnrmopn 21639 conndisj 21712 hausllycmp 21790 kqcldsat 22029 filufint 22216 cfinufil 22224 ufilen 22226 alexsublem 22340 bcth3 23621 inmbl 23830 iccmbl 23854 mbfimaicc 23919 i1fd 23969 itgss3 24102 difuncomp 29990 iundifdifd 29999 iundifdif 30000 pmtrcnelor 30390 cldssbrsiga 31059 unelcarsg 31183 kur14lem4 32066 cldbnd 33285 clsun 33287 mblfinlem3 34483 mblfinlem4 34484 ismblfin 34485 itg2addnclem 34495 fdc 34573 dssmapnvod 39872 sscon34b 39875 ntrclsfveq1 39916 ntrclsfveq 39918 ntrclsneine0lem 39920 ntrclsiso 39923 ntrclsk2 39924 ntrclskb 39925 ntrclsk3 39926 ntrclsk13 39927 ntrclsk4 39928 clsneiel2 39965 neicvgel2 39976 salincl 42172 salexct 42181 ovnsubadd2lem 42491 lincext2 44012 |
Copyright terms: Public domain | W3C validator |