| 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 4270. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
| Ref | Expression |
|---|---|
| dfss4 | ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝐴)) = 𝐴) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sseqin2 4223 | . 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∩ 𝐴) = 𝐴) | |
| 2 | eldif 3961 | . . . . . . 7 ⊢ (𝑥 ∈ (𝐵 ∖ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴)) | |
| 3 | 2 | notbii 320 | . . . . . 6 ⊢ (¬ 𝑥 ∈ (𝐵 ∖ 𝐴) ↔ ¬ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴)) |
| 4 | 3 | anbi2i 623 | . . . . 5 ⊢ ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ (𝐵 ∖ 𝐴)) ↔ (𝑥 ∈ 𝐵 ∧ ¬ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴))) |
| 5 | elin 3967 | . . . . . 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 4128 | . . 3 ⊢ (𝐵 ∖ (𝐵 ∖ 𝐴)) = (𝐵 ∩ 𝐴) |
| 12 | 11 | eqeq1i 2742 | . 2 ⊢ ((𝐵 ∖ (𝐵 ∖ 𝐴)) = 𝐴 ↔ (𝐵 ∩ 𝐴) = 𝐴) |
| 13 | 1, 12 | bitr4i 278 | 1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝐴)) = 𝐴) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∈ wcel 2108 ∖ cdif 3948 ∩ cin 3950 ⊆ wss 3951 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-3an 1089 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 df-v 3482 df-dif 3954 df-in 3958 df-ss 3968 |
| This theorem is referenced by: ssdifim 4273 dfin4 4278 sscon34b 4304 sorpsscmpl 7754 sbthlem3 9125 fin23lem7 10356 fin23lem11 10357 compsscnvlem 10410 compssiso 10414 isf34lem4 10417 efgmnvl 19732 frlmlbs 21817 isopn2 23040 iincld 23047 iuncld 23053 clsval2 23058 ntrval2 23059 ntrdif 23060 clsdif 23061 cmclsopn 23070 opncldf1 23092 indiscld 23099 mretopd 23100 restcld 23180 pnrmopn 23351 conndisj 23424 hausllycmp 23502 kqcldsat 23741 filufint 23928 cfinufil 23936 ufilen 23938 alexsublem 24052 bcth3 25365 inmbl 25577 iccmbl 25601 mbfimaicc 25666 i1fd 25716 itgss3 25850 difuncomp 32566 iundifdifd 32574 iundifdif 32575 supppreima 32700 pmtrcnelor 33111 ist0cld 33832 cldssbrsiga 34188 unelcarsg 34314 kur14lem4 35214 cldbnd 36327 clsun 36329 mblfinlem3 37666 mblfinlem4 37667 ismblfin 37668 itg2addnclem 37678 fdc 37752 dssmapnvod 44033 ntrclsfveq1 44073 ntrclsfveq 44075 ntrclsneine0lem 44077 ntrclsiso 44080 ntrclsk2 44081 ntrclskb 44082 ntrclsk3 44083 ntrclsk13 44084 ntrclsk4 44085 clsneiel2 44122 neicvgel2 44133 salincl 46339 salexct 46349 ovnsubadd2lem 46660 lincext2 48372 opncldeqv 48799 |
| Copyright terms: Public domain | W3C validator |