Colors of
variables: wff
setvar class |
Syntax hints:
= wceq 1539 ∪ cun 3945 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911
ax-6 1969 ax-7 2009 ax-8 2106
ax-9 2114 ax-ext 2701 |
This theorem depends on definitions:
df-bi 206 df-an 395
df-or 844 df-tru 1542 df-ex 1780 df-sb 2066 df-clab 2708 df-cleq 2722 df-clel 2808 df-v 3474 df-un 3952 |
This theorem is referenced by: disjssun
4466 difprsn1
4802 unidmrn
6277 phplem1OLD
9219 djucomen
10174 ackbij1lem14
10230 ltxrlt
11288 ruclem6
16182 ruclem7
16183 i1f1
25439 vtxdgoddnumeven
29077 subfacp1lem1
34468 lindsenlbs
36786 poimirlem6
36797 poimirlem7
36798 poimirlem16
36807 poimirlem17
36808 pwfi2f1o
42140 cnvrcl0
42678 iunrelexp0
42755 dfrtrcl4
42791 cotrclrcl
42795 dffrege76
42992 sucidALTVD
43933 sucidALT
43934 |