Colors of
variables: wff
setvar class |
Syntax hints:
= wceq 1540 ∩ cin 3947 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912
ax-6 1970 ax-7 2010 ax-8 2107
ax-9 2115 ax-ext 2702 |
This theorem depends on definitions:
df-bi 206 df-an 396
df-tru 1543 df-ex 1781 df-sb 2067 df-clab 2709 df-cleq 2723 df-clel 2809 df-rab 3432 df-v 3475 df-in 3955 |
This theorem is referenced by: difindir
4282 resindir
5998 predin
6328 restbas
22883 connsuba
23145 kgentopon
23263 trfbas2
23568 trfil2
23612 fclsrest
23749 trust
23955 chtdif
26899 ppidif
26904 mdslmd1lem1
31846 mdslmd1lem2
31847 mddmdin0i
31952 ballotlemgun
33822 cvmsss2
34564 |