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 5220 | . 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∖ 𝐵) ∈ V) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝐴 ∖ 𝐵) ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2110 Vcvv 3408 ∖ cdif 3863 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-ext 2708 ax-sep 5192 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1546 df-ex 1788 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3070 df-v 3410 df-dif 3869 df-in 3873 df-ss 3883 |
This theorem is referenced by: ralxpmap 8577 domdifsn 8728 domunsncan 8745 mapdom2 8817 acni 9659 infdif 9823 infpss 9831 enfin1ai 9998 fpwwe2 10257 canthp1lem1 10266 hashf1lem1 14020 mrieqv2d 17142 mreexexlemd 17147 dpjidcl 19445 pnrmopn 22240 cmpfi 22305 csdfil 22791 ufileu 22816 filufint 22817 alexsublem 22941 bcth3 24228 iunmbl 24450 tdeglem4 24957 gsummptres2 31032 tocycfv 31095 cyc3conja 31143 esummono 31734 esumpad 31735 esumpad2 31736 insiga 31817 sexp2 33530 sexp3 33536 selvval2lemn 39940 selvval2lem4 39941 selvval2lem5 39942 selvcl 39943 fsuppssind 39992 clcnvlem 40907 dssmapfv3d 41304 dssmapnvod 41305 ovolsplit 43204 intsal 43544 sge0ss 43625 sge0fodjrnlem 43629 iundjiun 43673 meaiunlelem 43681 iscnrm3rlem7 45913 |
Copyright terms: Public domain | W3C validator |