Colors of
variables: wff
setvar class |
Syntax hints: ∀wal 1539 Ⅎwnf 1785
∈ wcel 2106 ∃*wrmo 3375 Disj wdisj 5113 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913
ax-6 1971 ax-7 2011 ax-10 2137 ax-11 2154 ax-12 2171 |
This theorem depends on definitions:
df-bi 206 df-or 846
df-ex 1782 df-nf 1786 df-mo 2534 df-rmo 3376 df-disj 5114 |
This theorem is referenced by: disjabrex
32068 disjabrexf
32069 hasheuni
33369 ldgenpisyslem1
33447 measvunilem
33496 measvunilem0
33497 measvuni
33498 measinblem
33504 voliune
33513 volfiniune
33514 volmeas
33515 dstrvprob
33756 ismeannd
45482 |