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
12996 fsumcom2
15595 fprodcom2
15803 0rest
17247 firest
17250 2oppchomf
17542 isinv
17579 invsym2
17582 invfun
17583 oppcsect2
17598 oppcinv
17599 oppchofcl
18085 oyoncl
18095 clatl
18333 gicer
19001 gsum2d2lem
19685 gsum2d2
19686 gsumcom2
19687 gsumxp
19688 dprd2d2
19758 mattpostpos
21731 mdetunilem9
21897 restbas
22437 txuni2
22844 txcls
22883 txdis1cn
22914 txkgen
22931 hmpher
23063 cnextrel
23342 tgphaus
23396 qustgplem
23400 tsmsxp
23434 utop2nei
23530 utop3cls
23531 xmeter
23714 caubl
24600 ovoliunlem1
24794 reldv
25162 taylf
25648 lgsquadlem1
26656 lgsquadlem2
26657 nvrel
29349 dfcnv2
31396 gsumpart
31698 qusxpid
31951 qtophaus
32197 cvmliftlem1
33659 cvmlift2lem12
33688 gonan0
33766 xpab
34079 dfso2
34122 frxp2
34183 frxp3
34189 relbigcup
34413 poimirlem3
36012 heicant
36044 vvdifopab
36651 cnvref4
36742 dvhopellsm
39511 dibvalrel
39557 dib1dim
39559 diclspsn
39588 dih1
39680 dih1dimatlem
39723 aoprssdm
45225 eliunxp2
46200 joindm2
46792 meetdm2
46794 |