Colors of
variables: wff
setvar class |
Syntax hints:
= wceq 1539 ∖ cdif 3944 |
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-ex 1780 df-sb 2066 df-clab 2708 df-cleq 2722 df-clel 2808 df-rab 3431 df-dif 3950 |
This theorem is referenced by: indifdir
4283 difrab
4307 resdifdi
6234 resdifdir
6235 preddif
6329 infdju1
10186 uniioombllem4
25335 new0
27606 clwwlknclwwlkdif
29499 gtiso
32189 satffunlem2lem2
34695 mthmpps
34871 zrdivrng
37124 isdrngo1
37127 pwfi2f1o
42140 salexct2
45353 dfnelbr2
46279 |