| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > difexd | Structured version Visualization version GIF version | ||
| Description: Existence of a difference. (Contributed by SN, 16-Jul-2024.) |
| Ref | Expression |
|---|---|
| difexd.1 | ⊢ (𝜑 → 𝐴 ∈ 𝑉) |
| Ref | Expression |
|---|---|
| difexd | ⊢ (𝜑 → (𝐴 ∖ 𝐵) ∈ V) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | difexd.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ 𝑉) | |
| 2 | difexg 5329 | . 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∖ 𝐵) ∈ V) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝐴 ∖ 𝐵) ∈ V) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ 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: sexp2 8171 sexp3 8178 ralxpmap 8936 domdifsn 9094 domunsncan 9112 mapdom2 9188 acni 10085 infdif 10248 infpss 10256 enfin1ai 10424 fpwwe2 10683 canthp1lem1 10692 hashf1lem1 14494 mrieqv2d 17682 mreexexlemd 17687 dpjidcl 20078 pnrmopn 23351 cmpfi 23416 csdfil 23902 ufileu 23927 filufint 23928 alexsublem 24052 bcth3 25365 iunmbl 25588 tdeglem4 26099 fdifsupp 32694 gsummptres2 33056 tocycfv 33129 cyc3conja 33177 rprmdvdsprod 33562 esummono 34055 esumpad 34056 esumpad2 34057 insiga 34138 selvcllemh 42590 selvcllem4 42591 selvcllem5 42592 selvcl 42593 selvval2 42594 selvvvval 42595 selvadd 42598 selvmul 42599 fsuppssind 42603 tfsconcatun 43350 oaun2 43394 oaun3 43395 clcnvlem 43636 dssmapfv3d 44032 dssmapnvod 44033 ovolsplit 46003 intsal 46345 sge0ss 46427 sge0fodjrnlem 46431 iundjiun 46475 meaiunlelem 46483 iscnrm3rlem7 48843 |
| Copyright terms: Public domain | W3C validator |