Colors of
variables: wff
setvar class |
Syntax hints: ∀wal 1540 Ⅎwnf 1786
∈ wcel 2107 ∃*wrmo 3376 Disj wdisj 5114 |
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-10 2138 ax-11 2155 ax-12 2172 |
This theorem depends on definitions:
df-bi 206 df-or 847
df-ex 1783 df-nf 1787 df-mo 2535 df-rmo 3377 df-disj 5115 |
This theorem is referenced by: disjabrex
31813 disjabrexf
31814 hasheuni
33083 ldgenpisyslem1
33161 measvunilem
33210 measvunilem0
33211 measvuni
33212 measinblem
33218 voliune
33227 volfiniune
33228 volmeas
33229 dstrvprob
33470 ismeannd
45183 |