Colors of
variables: wff
setvar class |
Syntax hints: -> wi 4 <-> wb 184
= wceq 1395 e. wcel 1818 E. wrex 2808
[. wsbc 3327 { csn 4029 |
This theorem is referenced by: rexsn
4069 rexprg
4079 rextpg
4081 iunxsng
4409 frirr
4861 frsn
5075 imasng
5364 scshwfzeqfzo
12794 mnd1
15961 mnd1OLD
15962 grp1
16142 frgra2v
24999 1vwmgra
25003 ballotlemfc0
28431 ballotlemfcc
28432 zlidlring
32734 lco0
33028 elpaddat
35528 elpadd2at
35530 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1618 ax-4 1631 ax-5 1704
ax-6 1747 ax-7 1790 ax-10 1837 ax-12 1854 ax-13 1999 ax-ext 2435 |
This theorem depends on definitions:
df-bi 185 df-an 371
df-3an 975 df-tru 1398 df-ex 1613 df-nf 1617 df-sb 1740 df-clab 2443 df-cleq 2449 df-clel 2452 df-rex 2813 df-v 3111 df-sbc 3328 df-sn 4030 |