Colors of
variables: wff
setvar class |
Syntax hints:
= wceq 1542 ∖ cdif 3946 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914
ax-6 1972 ax-7 2012 ax-8 2109
ax-9 2117 ax-ext 2704 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-rab 3434 df-dif 3952 |
This theorem is referenced by: indifdir
4285 difrab
4309 resdifdi
6236 resdifdir
6237 preddif
6331 infdju1
10184 uniioombllem4
25103 new0
27369 clwwlknclwwlkdif
29232 gtiso
31922 satffunlem2lem2
34397 mthmpps
34573 zrdivrng
36821 isdrngo1
36824 pwfi2f1o
41838 salexct2
45055 dfnelbr2
45981 |