Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∧ wa 397
⊆ wss 3949 |
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 |
This theorem is referenced by: intssuni2
4978 marypha1
9429 cardinfima
10092 cfflb
10254 ssfin4
10305 acsfn
17603 mrelatlub
18515 efgval
19585 islbs3
20768 kgentopon
23042 txlly
23140 sigaclci
33130 bnj1014
33972 topjoin
35250 filnetlem3
35265 poimirlem16
36504 mblfinlem3
36527 sspwimpALT
43686 sspwimpALT2
43689 setrecsres
47747 |