Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ↔ wb 205
∧ wa 396 = wceq 1540
∈ wcel 2105 –1-1→wf1 6476
‘cfv 6479 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912
ax-6 1970 ax-7 2010 ax-8 2107
ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2707 ax-sep 5243 ax-nul 5250 ax-pr 5372 |
This theorem depends on definitions:
df-bi 206 df-an 397
df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-ne 2941 df-ral 3062 df-rex 3071 df-rab 3404 df-v 3443 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-nul 4270 df-if 4474 df-sn 4574 df-pr 4576 df-op 4580 df-uni 4853 df-br 5093 df-opab 5155 df-id 5518 df-xp 5626 df-rel 5627 df-cnv 5628 df-co 5629 df-dm 5630 df-iota 6431 df-fun 6481 df-fn 6482 df-f 6483 df-f1 6484 df-fv 6487 |
This theorem is referenced by: f1elima
7192 f1dom3fv3dif
7197 cocan1
7219 isof1oidb
7251 isosolem
7274 f1oiso
7278 weniso
7281 f1oweALT
7883 2dom
8895 xpdom2
8932 wemapwe
9554 fseqenlem1
9881 dfac12lem2
10001 infpssrlem4
10163 fin23lem28
10197 isf32lem7
10216 iundom2g
10397 canthnumlem
10505 canthwelem
10507 canthp1lem2
10510 pwfseqlem4
10519 seqf1olem1
13863 bitsinv2
16249 bitsf1
16252 sadasslem
16276 sadeq
16278 bitsuz
16280 eulerthlem2
16580 f1ocpbllem
17332 f1ovscpbl
17334 fthi
17731 ghmf1
18959 f1omvdmvd
19147 odf1
19265 dprdf1o
19730 zntoslem
20870 iporthcom
20946 ply1scln0
21568 cnt0
22603 cnhaus
22611 imasdsf1olem
23632 imasf1oxmet
23634 dyadmbl
24870 vitalilem3
24880 dvcnvlem
25246 facth1
25435 usgredg2v
27883 cycpmco2lem6
31685 erdszelem9
33460 cvmliftmolem1
33542 msubff1
33817 metf1o
36018 rngoisocnv
36244 laut11
38354 gicabl
41187 fourierdlem50
44033 |