Colors of
variables: wff set class |
Syntax hints:
→ wi 4 ↔ wb 105
∀wal 1351 = wceq 1353
∈ wcel 2148 {cab 2163 |
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 |
This theorem is referenced by: sbab
2305 iftrue
3541 iffalse
3544 iniseg
5002 fncnvima2
5639 isoini
5821 dftpos3
6265 unfiexmid
6919 tgval3
13643 txrest
13861 cnblcld
14120 |