Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∧ wa 397
∈ wcel 2107 𝒫
cpw 4564 |
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-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3449 df-in 3921 df-ss 3931 df-pw 4566 |
This theorem is referenced by: unipw
5411 axdc2lem
10392 axdc3lem4
10397 homarel
17930 txdis
23006 uhgredgrnv
28130 fpwrelmap
31704 insiga
32800 measinblem
32883 ddemeas
32899 imambfm
32926 totprobd
33090 dstrvprob
33135 ballotlem2
33152 requad2
45905 scmsuppss
46538 lincvalsc0
46592 linc0scn0
46594 lincdifsn
46595 linc1
46596 lincsum
46600 lincscm
46601 lcoss
46607 lincext3
46627 islindeps2
46654 itscnhlinecirc02p
46961 |