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
10445 axdc3lem4
10450 homarel
17990 txdis
23356 uhgredgrnv
28645 fpwrelmap
32213 insiga
33421 measinblem
33504 ddemeas
33520 imambfm
33547 totprobd
33711 dstrvprob
33756 ballotlem2
33773 requad2
46590 scmsuppss
47137 lincvalsc0
47190 linc0scn0
47192 lincdifsn
47193 linc1
47194 lincsum
47198 lincscm
47199 lcoss
47205 lincext3
47225 islindeps2
47252 itscnhlinecirc02p
47559 |