Colors of
variables: wff set class |
Syntax hints:
→ wi 4 = wceq 1353
⊆ wss 3130 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-7 1448
ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-11 1506 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 |
This theorem depends on definitions:
df-bi 117 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-in 3136 df-ss 3143 |
This theorem is referenced by: fssdm
5381 fndmdif
5622 fneqeql2
5626 fconst4m
5737 f1opw2
6077 ecss
6576 fopwdom
6836 ssenen
6851 phplem2
6853 fiintim
6928 casefun
7084 caseinj
7088 djufun
7103 djuinj
7105 nn0supp
9228 monoord2
10477 binom1dif
11495 cnpnei
13722 cnntri
13727 cnntr
13728 cncnp
13733 cndis
13744 txdis1cn
13781 hmeontr
13816 hmeoimaf1o
13817 dvcoapbr
14174 |