Colors of
variables: wff set class |
Syntax hints:
→ wi 4 = wceq 1353
⊆ wss 3129 |
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 3135 df-ss 3142 |
This theorem is referenced by: fssdm
5380 fndmdif
5621 fneqeql2
5625 fconst4m
5736 f1opw2
6076 ecss
6575 fopwdom
6835 ssenen
6850 phplem2
6852 fiintim
6927 casefun
7083 caseinj
7087 djufun
7102 djuinj
7104 nn0supp
9227 monoord2
10476 binom1dif
11494 cnpnei
13689 cnntri
13694 cnntr
13695 cncnp
13700 cndis
13711 txdis1cn
13748 hmeontr
13783 hmeoimaf1o
13784 dvcoapbr
14141 |