Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∧ wa 396
∈ wcel 2106 𝒫
cpw 4602 |
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-8 2108
ax-9 2116 ax-ext 2703 |
This theorem depends on definitions:
df-bi 206 df-an 397
df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-v 3476 df-in 3955 df-ss 3965 df-pw 4604 |
This theorem is referenced by: unipw
5450 axdc2lem
10442 axdc3lem4
10447 homarel
17985 txdis
23135 uhgredgrnv
28387 fpwrelmap
31953 insiga
33130 measinblem
33213 ddemeas
33229 imambfm
33256 totprobd
33420 dstrvprob
33465 ballotlem2
33482 requad2
46281 scmsuppss
47038 lincvalsc0
47092 linc0scn0
47094 lincdifsn
47095 linc1
47096 lincsum
47100 lincscm
47101 lcoss
47107 lincext3
47127 islindeps2
47154 itscnhlinecirc02p
47461 |