Colors of
variables: wff
setvar class |
Syntax hints: ¬ wn 3 ∈ wcel 2104
≠ wne 2938 ∖
cdif 3944 {csn 4627 |
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 1911
ax-6 1969 ax-7 2009 ax-8 2106
ax-9 2114 ax-ext 2701 |
This theorem depends on definitions:
df-bi 206 df-an 395
df-tru 1542 df-ex 1780 df-sb 2066 df-clab 2708 df-cleq 2722 df-clel 2808 df-ne 2939 df-v 3474 df-dif 3950 df-sn 4628 |
This theorem is referenced by: neldifsnd
4795 fofinf1o
9329 dfac9
10133 xrsupss
13292 hashgt23el
14388 fvsetsid
17105 islbs3
20913 islindf4
21612 ufinffr
23653 i1fd
25430 finsumvtxdg2sstep
29073 matunitlindflem1
36787 poimirlem25
36816 itg2addnclem
36842 itg2addnclem2
36843 prter2
38054 |