Colors of
variables: wff
setvar class |
Syntax hints: class class
class wbr 5109 ◡ccnv 5636
Rel wrel 5642 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914
ax-6 1972 ax-7 2012 ax-8 2109
ax-9 2117 ax-ext 2704 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3449 df-in 3921 df-ss 3931 df-opab 5172 df-xp 5643 df-rel 5644 df-cnv 5645 |
This theorem is referenced by: relbrcnvg
6061 eliniseg2
6062 cnvsym
6070 cnvsymOLD
6071 cnvsymOLDOLD
6072 intasym
6073 asymref
6074 cnvopab
6095 cnvdif
6100 dfrel2
6145 cnvcnv
6148 cnvsn0
6166 cnvcnvsn
6175 resdm2
6187 coi2
6219 coires1
6220 cnvssrndm
6227 unidmrn
6235 cnviin
6242 predep
6288 funi
6537 funcnvsn
6555 funcnv2
6573 fcnvres
6723 f1cnvcnv
6752 f1ompt
7063 fliftcnv
7260 cnvexg
7865 cnvf1o
8047 fsplit
8053 reldmtpos
8169 dmtpos
8173 rntpos
8174 dftpos3
8179 dftpos4
8180 tpostpos
8181 tposf12
8186 ercnv
8675 cnvct
8984 omxpenlem
9023 domss2
9086 cnvfi
9130 cnvfiALT
9284 trclublem
14889 relexpaddg
14947 fsumcnv
15666 fsumcom2
15667 fprodcnv
15874 fprodcom2
15875 invsym2
17654 oppcsect2
17670 cnvps
18475 tsrdir
18501 mvdco
19235 gsumcom2
19760 funcnvmpt
31636 fcnvgreu
31642 dfcnv2
31645 gsummpt2co
31946 gsumhashmul
31954 cnvco1
34395 cnvco2
34396 colinrel
34695 trer
34841 releleccnv
36767 eleccnvep
36791 brcnvrabga
36853 cnvresrn
36859 ineccnvmo
36868 elec1cnvxrn2
36909 cnvelrels
37007 dfdisjALTV
37225 dfeldisj5
37233 dfantisymrel4
37273 dfantisymrel5
37274 cnvnonrel
41952 cnvcnvintabd
41964 cnvintabd
41967 cnvssco
41970 clrellem
41986 clcnvlem
41987 cnviun
42014 trrelsuperrel2dg
42035 dffrege115
42342 |