Colors of
variables: wff set class |
Syntax hints:
∧ wa 104 ↔ wb 105
∃wrex 2456 |
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 ax-ie1 1493 ax-ie2 1494 ax-4 1510 ax-17 1526 ax-ial 1534 |
This theorem depends on definitions:
df-bi 117 df-nf 1461 df-rex 2461 |
This theorem is referenced by: r19.42v
2634 3reeanv
2648 reuind
2943 iuncom4
3894 dfiun2g
3919 iunxiun
3969 inuni
4156 xpiundi
4685 xpiundir
4686 imaco
5135 coiun
5139 abrexco
5760 imaiun
5761 isoini
5819 rexrnmpo
5990 mapsnen
6811 genpassl
7523 genpassu
7524 4fvwrd4
10140 metrest
14009 trirec0xor
14796 |