Colors of
variables: wff
setvar class |
Syntax hints:
= wceq 1542 ∖ cdif 3908 |
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 3407 df-dif 3914 |
This theorem is referenced by: indifdir
4245 difrab
4269 resdifdi
6189 resdifdir
6190 preddif
6284 infdju1
10130 uniioombllem4
24966 new0
27226 clwwlknclwwlkdif
28965 gtiso
31661 satffunlem2lem2
34057 mthmpps
34233 zrdivrng
36458 isdrngo1
36461 pwfi2f1o
41466 salexct2
44666 dfnelbr2
45591 |