Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∧ wa 397
∈ wcel 2107 𝒫
cpw 4603 |
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 3477 df-in 3956 df-ss 3966 df-pw 4605 |
This theorem is referenced by: unipw
5451 axdc2lem
10443 axdc3lem4
10448 homarel
17986 txdis
23136 uhgredgrnv
28390 fpwrelmap
31958 insiga
33135 measinblem
33218 ddemeas
33234 imambfm
33261 totprobd
33425 dstrvprob
33470 ballotlem2
33487 requad2
46291 scmsuppss
47048 lincvalsc0
47102 linc0scn0
47104 lincdifsn
47105 linc1
47106 lincsum
47110 lincscm
47111 lcoss
47117 lincext3
47137 islindeps2
47164 itscnhlinecirc02p
47471 |