Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∧ wa 396
∈ wcel 2106 ◡ccnv 5630
⟶wf 6489 –1-1-onto→wf1o 6492 ‘cfv 6493 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913
ax-6 1971 ax-7 2011 ax-8 2108
ax-9 2116 ax-10 2137 ax-12 2171 ax-ext 2707 ax-sep 5254 ax-nul 5261 ax-pr 5382 |
This theorem depends on definitions:
df-bi 206 df-an 397
df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-ne 2942 df-ral 3063 df-rex 3072 df-rab 3406 df-v 3445 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4281 df-if 4485 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4864 df-br 5104 df-opab 5166 df-id 5529 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-iota 6445 df-fun 6495 df-fn 6496 df-f 6497 df-f1 6498 df-fo 6499 df-f1o 6500 df-fv 6501 |
This theorem is referenced by: f1oiso2
7293 f1ocnvfv3
7348 dif1enlem
9096 dif1enlemOLD
9097 rexdif1en
9098 rexdif1enOLD
9099 dif1en
9100 dif1enOLD
9102 uzrdglem
13854 uzrdgsuci
13857 fzennn
13865 cardfz
13867 fzfi
13869 iunmbl2
24905 f1otrg
27699 axcontlem10
27808 wlkiswwlks2lem5
28704 clwlkclwwlklem2a
28828 cnvbraval
30938 cnvbracl
30939 cycpmco2lem6
31863 cycpmco2
31865 mndpluscn
32376 ismtycnv
36228 rngoisocnv
36407 lautcnvclN
38518 lautcnvle
38519 lautcvr
38522 lautj
38523 lautm
38524 ltrncnvatb
38568 diacnvclN
39481 dihcnvcl
39701 dihlspsnat
39763 dihglblem6
39770 dochocss
39796 dochnoncon
39821 mapdcnvcl
40082 rmxyelxp
41174 cantnfub
41593 isomuspgrlem1
45951 isomgrsym
45960 |