Colors of
variables: wff
setvar class |
Syntax hints: <-> wb 184 /\ wa 369
e. wcel 1818 i^i cin 3474 <. cop 4035
class class class wbr 4452 |
This theorem is referenced by: brinxp2
5066 trin2
5395 poirr2
5396 tpostpos
6994 erinxp
7404 sbthcl
7659 infxpenlem
8412 fpwwe2lem12
9040 fpwwe2
9042 isinv
15154 isffth2
15285 ffthf1o
15288 ffthoppc
15293 ffthres2c
15309 isunit
17306 opsrtoslem2
18149 posrasymb
27645 trleile
27654 dfpo2
29184 brtxp
29530 idsset
29540 dfon3
29542 elfix
29553 dffix2
29555 brcap
29590 funpartlem
29592 trer
30134 fneval
30170 |
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-11 1842 ax-12 1854 ax-13 1999 ax-ext 2435 |
This theorem depends on definitions:
df-bi 185 df-an 371
df-tru 1398 df-ex 1613 df-nf 1617 df-sb 1740 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-v 3111 df-in 3482 df-br 4453 |