Colors of
variables: wff setvar class |
Syntax hints: →
wi 4 = wceq 1642
∈ wcel 1710 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675
ax-11 1746 ax-ext 2334 |
This theorem depends on definitions:
df-bi 177 df-an 360
df-ex 1542 df-cleq 2346 df-clel 2349 |
This theorem is referenced by: syl6eqelr
2442 snex
4112 sikss1c1c
4268 ins2kss
4280 ins3kss
4281 iotaex
4357 eladdc
4399 ssfin
4471 f0cli
5419 elimdelov
5574 ndmovcl
5615 brfns
5834 muccl
6133 ncaddccl
6145 ceclb
6184 cet
6235 nclenn
6250 nchoicelem12
6301 nchoicelem17
6306 nchoicelem18
6307 nchoicelem19
6308 |