| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > difexi | Structured version Visualization version GIF version | ||
| Description: Existence of a difference, inference version of difexg 5329. (Contributed by Glauco Siliprandi, 3-Mar-2021.) (Revised by AV, 26-Mar-2021.) |
| Ref | Expression |
|---|---|
| difexi.1 | ⊢ 𝐴 ∈ V |
| Ref | Expression |
|---|---|
| difexi | ⊢ (𝐴 ∖ 𝐵) ∈ V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | difexi.1 | . 2 ⊢ 𝐴 ∈ V | |
| 2 | difexg 5329 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∖ 𝐵) ∈ V) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∖ 𝐵) ∈ V |
| Colors of variables: wff setvar class |
| Syntax hints: ∈ wcel 2108 Vcvv 3480 ∖ cdif 3948 |
| 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 ax-sep 5296 |
| 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: oev 8552 naddcllem 8714 sbthlem2 9124 findcard 9203 findcard2 9204 pssnn 9208 ssfi 9213 phplem2OLD 9255 phpOLD 9259 frfi 9321 unfilem3 9345 marypha1lem 9473 wemapso 9591 inf3lem3 9670 dfac9 10177 dfacacn 10182 kmlem11 10201 kmlem12 10202 fin23lem28 10380 isf32lem6 10398 isf32lem7 10399 isf32lem8 10400 domtriomlem 10482 axdc2lem 10488 axcclem 10497 zornn0g 10545 konigthlem 10608 grothprim 10874 hashbclem 14491 fi1uzind 14546 brfi1uzind 14547 brfi1indALT 14549 opfi1uzind 14550 ramub1lem1 17064 pltfval 18376 isirred 20419 cntzsdrg 20803 subdrgint 20804 lssset 20931 xrs1mnd 21422 xrs10 21423 xrs1cmn 21424 xrge0subm 21425 xrge0cmn 21426 cnmsgngrp 21597 psgninv 21600 psdmul 22170 neitr 23188 lecldbas 23227 imasdsf1olem 24383 xrge0gsumle 24855 xrge0tsms 24856 i1fd 25716 lhop1lem 26052 reefgim 26494 cxpcn2 26789 logbmpt 26831 newval 27894 newf 27897 addsval 27995 mulsval 28135 nnsex 28323 axlowdimlem15 28971 axlowdim 28976 elntg 28999 uhgrspan1lem1 29317 upgrres1lem1 29326 nbgrval 29353 nbfusgrlevtxm1 29394 cusgrfilem3 29475 vtxdginducedm1lem1 29557 vtxdginducedm1fi 29562 finsumvtxdg2ssteplem4 29566 rprmval 33544 dimkerim 33678 satfv1lem 35367 satfdm 35374 satffunlem1lem2 35408 satffunlem2lem2 35411 watvalN 39995 hvmapfval 41761 prjspval 42613 setindtr 43036 ssdifcl 43584 sssymdifcl 43585 clsk3nimkb 44053 iundjiunlem 46474 meaiuninclem 46495 meaiininclem 46501 lines 48652 |
| Copyright terms: Public domain | W3C validator |