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 4233. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
Ref | Expression |
---|---|
dfss4 | ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝐴)) = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sseqin2 4189 | . 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∩ 𝐴) = 𝐴) | |
2 | eldif 3943 | . . . . . . 7 ⊢ (𝑥 ∈ (𝐵 ∖ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴)) | |
3 | 2 | notbii 321 | . . . . . 6 ⊢ (¬ 𝑥 ∈ (𝐵 ∖ 𝐴) ↔ ¬ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴)) |
4 | 3 | anbi2i 622 | . . . . 5 ⊢ ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ (𝐵 ∖ 𝐴)) ↔ (𝑥 ∈ 𝐵 ∧ ¬ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴))) |
5 | elin 4166 | . . . . . 6 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴)) | |
6 | abai 822 | . . . . . 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 4098 | . . 3 ⊢ (𝐵 ∖ (𝐵 ∖ 𝐴)) = (𝐵 ∩ 𝐴) |
12 | 11 | eqeq1i 2823 | . 2 ⊢ ((𝐵 ∖ (𝐵 ∖ 𝐴)) = 𝐴 ↔ (𝐵 ∩ 𝐴) = 𝐴) |
13 | 1, 12 | bitr4i 279 | 1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝐴)) = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∧ wa 396 = wceq 1528 ∈ wcel 2105 ∖ cdif 3930 ∩ cin 3932 ⊆ wss 3933 |
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 2790 |
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 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-rab 3144 df-v 3494 df-dif 3936 df-in 3940 df-ss 3949 |
This theorem is referenced by: ssdifim 4236 dfin4 4241 sorpsscmpl 7449 sbthlem3 8617 fin23lem7 9726 fin23lem11 9727 compsscnvlem 9780 compssiso 9784 isf34lem4 9787 efgmnvl 18769 frlmlbs 20869 isopn2 21568 iincld 21575 iuncld 21581 clsval2 21586 ntrval2 21587 ntrdif 21588 clsdif 21589 cmclsopn 21598 opncldf1 21620 indiscld 21627 mretopd 21628 restcld 21708 pnrmopn 21879 conndisj 21952 hausllycmp 22030 kqcldsat 22269 filufint 22456 cfinufil 22464 ufilen 22466 alexsublem 22580 bcth3 23861 inmbl 24070 iccmbl 24094 mbfimaicc 24159 i1fd 24209 itgss3 24342 difuncomp 30232 iundifdifd 30241 iundifdif 30242 pmtrcnelor 30662 cldssbrsiga 31345 unelcarsg 31469 kur14lem4 32353 cldbnd 33571 clsun 33573 mblfinlem3 34812 mblfinlem4 34813 ismblfin 34814 itg2addnclem 34824 fdc 34901 dssmapnvod 40244 sscon34b 40247 ntrclsfveq1 40288 ntrclsfveq 40290 ntrclsneine0lem 40292 ntrclsiso 40295 ntrclsk2 40296 ntrclskb 40297 ntrclsk3 40298 ntrclsk13 40299 ntrclsk4 40300 clsneiel2 40337 neicvgel2 40348 salincl 42485 salexct 42494 ovnsubadd2lem 42804 lincext2 44438 |
Copyright terms: Public domain | W3C validator |