Colors of
variables: wff set class |
Syntax hints: wi 4
wb 105 wcel 2148 wral 2455 |
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-gen 1449 |
This theorem depends on definitions:
df-bi 117 df-ral 2460 |
This theorem is referenced by: frind
4352 poinxp
4695 soinxp
4696 seinxp
4697 dffun8
5244 funcnv3
5278 fncnv
5282 fnres
5332 fvreseq
5619 isoini2
5819 smores
6292 resixp
6732 pw1dc1
6912 finomni
7137 caucvgre
10989 xpscf
12765 bj-charfundcALT
14531 |