Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∧ wa 397
⊆ wss 3915 |
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 2708 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-v 3450 df-in 3922 df-ss 3932 |
This theorem is referenced by: intssuni2
4939 marypha1
9377 cardinfima
10040 cfflb
10202 ssfin4
10253 acsfn
17546 mrelatlub
18458 efgval
19506 islbs3
20632 kgentopon
22905 txlly
23003 sigaclci
32771 bnj1014
33613 topjoin
34866 filnetlem3
34881 poimirlem16
36123 mblfinlem3
36146 sspwimpALT
43281 sspwimpALT2
43284 setrecsres
47221 |