![]() |
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 4258. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
Ref | Expression |
---|---|
dfss4 | ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝐴)) = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sseqin2 4213 | . 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∩ 𝐴) = 𝐴) | |
2 | eldif 3954 | . . . . . . 7 ⊢ (𝑥 ∈ (𝐵 ∖ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴)) | |
3 | 2 | notbii 319 | . . . . . 6 ⊢ (¬ 𝑥 ∈ (𝐵 ∖ 𝐴) ↔ ¬ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴)) |
4 | 3 | anbi2i 621 | . . . . 5 ⊢ ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ (𝐵 ∖ 𝐴)) ↔ (𝑥 ∈ 𝐵 ∧ ¬ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴))) |
5 | elin 3960 | . . . . . 6 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴)) | |
6 | abai 825 | . . . . . 6 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴))) | |
7 | iman 400 | . . . . . . 7 ⊢ ((𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴) ↔ ¬ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴)) | |
8 | 7 | anbi2i 621 | . . . . . 6 ⊢ ((𝑥 ∈ 𝐵 ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)) ↔ (𝑥 ∈ 𝐵 ∧ ¬ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴))) |
9 | 5, 6, 8 | 3bitri 296 | . . . . 5 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ¬ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴))) |
10 | 4, 9 | bitr4i 277 | . . . 4 ⊢ ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ (𝐵 ∖ 𝐴)) ↔ 𝑥 ∈ (𝐵 ∩ 𝐴)) |
11 | 10 | difeqri 4120 | . . 3 ⊢ (𝐵 ∖ (𝐵 ∖ 𝐴)) = (𝐵 ∩ 𝐴) |
12 | 11 | eqeq1i 2730 | . 2 ⊢ ((𝐵 ∖ (𝐵 ∖ 𝐴)) = 𝐴 ↔ (𝐵 ∩ 𝐴) = 𝐴) |
13 | 1, 12 | bitr4i 277 | 1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝐴)) = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 394 = wceq 1533 ∈ wcel 2098 ∖ cdif 3941 ∩ cin 3943 ⊆ wss 3944 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-3an 1086 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-rab 3419 df-v 3463 df-dif 3947 df-in 3951 df-ss 3961 |
This theorem is referenced by: ssdifim 4261 dfin4 4266 sscon34b 4293 sorpsscmpl 7740 sbthlem3 9110 fin23lem7 10341 fin23lem11 10342 compsscnvlem 10395 compssiso 10399 isf34lem4 10402 efgmnvl 19681 frlmlbs 21748 isopn2 22980 iincld 22987 iuncld 22993 clsval2 22998 ntrval2 22999 ntrdif 23000 clsdif 23001 cmclsopn 23010 opncldf1 23032 indiscld 23039 mretopd 23040 restcld 23120 pnrmopn 23291 conndisj 23364 hausllycmp 23442 kqcldsat 23681 filufint 23868 cfinufil 23876 ufilen 23878 alexsublem 23992 bcth3 25303 inmbl 25515 iccmbl 25539 mbfimaicc 25604 i1fd 25654 itgss3 25788 difuncomp 32423 iundifdifd 32431 iundifdif 32432 supppreima 32553 pmtrcnelor 32904 ist0cld 33562 cldssbrsiga 33934 unelcarsg 34060 kur14lem4 34947 cldbnd 35938 clsun 35940 mblfinlem3 37260 mblfinlem4 37261 ismblfin 37262 itg2addnclem 37272 fdc 37346 dssmapnvod 43589 ntrclsfveq1 43629 ntrclsfveq 43631 ntrclsneine0lem 43633 ntrclsiso 43636 ntrclsk2 43637 ntrclskb 43638 ntrclsk3 43639 ntrclsk13 43640 ntrclsk4 43641 clsneiel2 43678 neicvgel2 43689 salincl 45847 salexct 45857 ovnsubadd2lem 46168 lincext2 47706 opncldeqv 48103 |
Copyright terms: Public domain | W3C validator |