Colors of
variables: wff setvar class |
Syntax hints: =
wceq 1642 ∩ cin 3209 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675
ax-6 1729 ax-7 1734 ax-11 1746 ax-12 1925 ax-ext 2334 |
This theorem depends on definitions:
df-bi 177 df-or 359
df-an 360 df-nan 1288 df-tru 1319 df-ex 1542 df-nf 1545 df-sb 1649 df-clab 2340 df-cleq 2346 df-clel 2349 df-nfc 2479 df-v 2862 df-nin 3212 df-compl 3213 df-in 3214 |
This theorem is referenced by: in4
3472 inindir
3474 indif2
3499 difun1
3515 dfrab3ss
3534 undif1
3626 difdifdir
3638 dfif3
3673 dfif5
3675 intunsn
3966 rint0
3967 riin0
4040 inindif
4076 ssfin
4471 spfinex
4538 res0
4978 resres
4981 resundi
4982 resindi
4984 inres
4986 resopab
5000 dminxp
5062 resdmres
5079 funimacnv
5169 sbthlem1
6204 |