Colors of
variables: wff
setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205
∧ wa 397 = wceq 1542
≠ wne 2944 ⊆
wss 3915 ⊊ wpss 3916 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-ne 2945 df-pss 3934 |
This theorem is referenced by: dfpss3
4051 sspss
4064 psstr
4069 npss
4075 ssnelpss
4076 pssv
4411 disj4
4423 f1imapss
7218 pssnn
9119 phpeqd
9166 phpeqdOLD
9176 nnsdomo
9185 pssnnOLD
9216 inf3lem6
9576 ssfin4
10253 fin23lem25
10267 fin23lem38
10292 isf32lem2
10297 pwfseqlem4
10605 genpcl
10951 prlem934
10976 ltaddpr
10977 sltlpss
27258 chnlei
30469 cvbr2
31267 cvnbtwn2
31271 cvnbtwn3
31272 cvnbtwn4
31273 dfon2lem3
34399 dfon2lem5
34401 dfon2lem6
34402 dfon2lem7
34403 dfon2lem8
34404 dfon3
34506 lcvbr2
37513 lcvnbtwn2
37518 lcvnbtwn3
37519 rr-phpd
42557 |