Colors of
variables: wff
setvar class |
Syntax hints:
↔ wb 205 ∈ wcel 2104
∃wrex 3068 Vcvv 3472
class class class wbr 5149 “ cima 5680 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911
ax-6 1969 ax-7 2009 ax-8 2106
ax-9 2114 ax-ext 2701 ax-sep 5300 ax-nul 5307 ax-pr 5428 |
This theorem depends on definitions:
df-bi 206 df-an 395
df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-sb 2066 df-clab 2708 df-cleq 2722 df-clel 2808 df-ral 3060 df-rex 3069 df-rab 3431 df-v 3474 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-sn 4630 df-pr 4632 df-op 4636 df-br 5150 df-opab 5212 df-xp 5683 df-cnv 5685 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 |
This theorem is referenced by: elima2
6066 rninxp
6179 imaco
6251 imaindm
6299 isarep1
6638 isarep1OLD
6639 eliman0
6932 funimass4
6957 isomin
7338 dfsup2
9443 dfac10b
10138 hausmapdom
23226 pi1blem
24788 scutun12
27546 madeval2
27583 adjbd1o
31603 brimage
35200 dfrecs2
35224 dfrdg4
35225 dfint3
35226 imagesset
35227 elimaint
42704 elintima
42708 |