Colors of
variables: wff
setvar class |
Syntax hints:
= wceq 1542 ∪ cun 3947 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914
ax-6 1972 ax-7 2012 ax-8 2109
ax-9 2117 ax-ext 2704 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-or 847 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3477 df-un 3954 |
This theorem is referenced by: disjssun
4468 difprsn1
4804 unidmrn
6279 phplem1OLD
9217 djucomen
10172 ackbij1lem14
10228 ltxrlt
11284 ruclem6
16178 ruclem7
16179 i1f1
25207 vtxdgoddnumeven
28810 subfacp1lem1
34170 lindsenlbs
36483 poimirlem6
36494 poimirlem7
36495 poimirlem16
36504 poimirlem17
36505 pwfi2f1o
41838 cnvrcl0
42376 iunrelexp0
42453 dfrtrcl4
42489 cotrclrcl
42493 dffrege76
42690 sucidALTVD
43631 sucidALT
43632 |