Colors of
variables: wff
setvar class |
Syntax hints: Vcvv 3444 ⊆ wss 3909
× cxp 5629 Rel wrel 5636 |
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 2709 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2716 df-cleq 2730 df-clel 2816 df-v 3446 df-in 3916 df-ss 3926 df-opab 5167 df-xp 5637 df-rel 5638 |
This theorem is referenced by: xpsspw
5762 relinxp
5767 xpiindi
5788 eliunxp
5790 opeliunxp2
5791 relres
5963 restidsing
6003 codir
6071 qfto
6072 difxp
6113 sofld
6136 cnvcnv
6141 dfco2
6194 unixp
6231 ressn
6234 fliftcnv
7251 fliftfun
7252 oprssdm
7528 frxp
8047 opeliunxp2f
8109 reltpos
8130 tposfo
8152 tposf
8153 swoer
8612 xpider
8661 xpcomf1o
8939 fpwwe2lem8
10508 ordpinq
10813 addassnq
10828 mulassnq
10829 distrnq
10831 mulidnq
10833 recmulnq
10834 ltexnq
10845 prcdnq
10863 ltrel
11151 lerel
11153 dfle2
12995 fsumcom2
15594 fprodcom2
15802 0rest
17246 firest
17249 2oppchomf
17541 isinv
17578 invsym2
17581 invfun
17582 oppcsect2
17597 oppcinv
17598 oppchofcl
18084 oyoncl
18094 clatl
18332 gicer
18999 gsum2d2lem
19680 gsum2d2
19681 gsumcom2
19682 gsumxp
19683 dprd2d2
19753 mattpostpos
21726 mdetunilem9
21892 restbas
22432 txuni2
22839 txcls
22878 txdis1cn
22909 txkgen
22926 hmpher
23058 cnextrel
23337 tgphaus
23391 qustgplem
23395 tsmsxp
23429 utop2nei
23525 utop3cls
23526 xmeter
23709 caubl
24595 ovoliunlem1
24789 reldv
25157 taylf
25643 lgsquadlem1
26651 lgsquadlem2
26652 nvrel
29343 dfcnv2
31390 gsumpart
31692 qusxpid
31945 qtophaus
32191 cvmliftlem1
33653 cvmlift2lem12
33682 gonan0
33760 xpab
34073 dfso2
34119 frxp2
34180 frxp3
34186 relbigcup
34378 poimirlem3
35977 heicant
36009 vvdifopab
36616 cnvref4
36707 dvhopellsm
39476 dibvalrel
39522 dib1dim
39524 diclspsn
39553 dih1
39645 dih1dimatlem
39688 aoprssdm
45189 eliunxp2
46164 joindm2
46756 meetdm2
46758 |