Colors of
variables: wff set class |
Syntax hints:
→ wi 4 ↔ wb 105 |
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-gen 1449 ax-ie2 1494 ax-8 1504 ax-17 1526 ax-i9 1530 ax-14 2151 |
This theorem depends on definitions:
df-bi 117 |
This theorem is referenced by: elsb2
2156 dveel2
2158 axext3
2160 axext4
2161 bm1.1
2162 eleq2w
2239 bm1.3ii
4126 nalset
4135 zfun
4436 fv3
5540 tfrlemisucaccv
6328 tfr1onlemsucaccv
6344 tfrcllemsucaccv
6357 acfun
7208 ccfunen
7265 cc1
7266 bdsepnft
14724 bdsepnfALT
14726 bdbm1.3ii
14728 bj-nalset
14732 bj-nnelirr
14790 nninfalllem1
14842 nninfsellemeq
14848 nninfsellemqall
14849 nninfsellemeqinf
14850 nninfomni
14853 |