Colors of
variables: wff
setvar class |
Syntax hints:
= wceq 1541 ∩ cin 3947 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913
ax-6 1971 ax-7 2011 ax-8 2108
ax-9 2116 ax-ext 2703 |
This theorem depends on definitions:
df-bi 206 df-an 397
df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-rab 3433 df-v 3476 df-in 3955 |
This theorem is referenced by: difindir
4282 resindir
5998 predin
6328 restbas
22661 connsuba
22923 kgentopon
23041 trfbas2
23346 trfil2
23390 fclsrest
23527 trust
23733 chtdif
26659 ppidif
26664 mdslmd1lem1
31573 mdslmd1lem2
31574 mddmdin0i
31679 ballotlemgun
33518 cvmsss2
34260 |