Colors of
variables: term |
Syntax hints: =
wb 1 C wc 3
∪ wo 6 ∩ wa 7 |
This theorem was proved from axioms:
ax-a1 30 ax-a2 31 ax-a3 32
ax-a4 33 ax-a5 34 ax-r1 35
ax-r2 36 ax-r4 37 ax-r5 38
ax-r3 439 |
This theorem depends on definitions:
df-b 39 df-a 40 df-t 41
df-f 42 df-le1 130 df-le2 131 df-c1 132
df-c2 133 |
This theorem is referenced by: fh1rc
479 gsth
489 dfi3b
499 ud3lem1b
567 ud3lem1d
569 ud3lem3d
575 ud5lem1a
586 ud5lem3a
591 u1lemaa
600 u3lemaa
602 u4lemaa
603 u5lemaa
604 u3lemana
607 u4lemana
608 u5lemana
609 u3lemab
612 u4lemab
613 u5lemab
614 u2lemanb
616 u4lemanb
618 u5lemanb
619 u4lem4
759 u4lem5
764 u5lem5
765 u5lem6
769 u1lem8
776 u3lem15
795 bi1o1a
798 3vded21
817 1oa
820 neg3antlem2
865 mhlem
876 mhlem1
877 marsdenlem3
882 marsdenlem4
883 |