Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 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-rel 5638 |
This theorem is referenced by: relin1
5765 relin2
5766 reldif
5768 relres
5963 iss
5986 cnvdif
6093 difxp
6113 sofld
6136 funss
6516 funssres
6541 fliftcnv
7251 fliftfun
7252 releldmdifi
7967 frxp
8047 reltpos
8130 swoer
8612 sbthcl
8973 fpwwe2lem8
10508 recmulnq
10834 prcdnq
10863 ltrel
11151 lerel
11153 dfle2
12995 dflt2
12996 isinv
17578 invsym2
17581 invfun
17582 oppcsect2
17597 oppcinv
17598 relfull
17730 relfth
17731 psss
18404 gicer
18999 gsum2d
19679 isunit
20010 txdis1cn
22909 hmpher
23058 tgphaus
23391 qustgplem
23395 tsmsxp
23429 xmeter
23709 ovoliunlem1
24789 taylf
25643 lgsquadlem1
26651 lgsquadlem2
26652 nvrel
29343 phrel
29556 bnrel
29608 hlrel
29631 gonan0
33760 frxp2
34180 frxp3
34186 sscoid
34394 trer
34684 fneer
34721 heicant
36009 iss2
36701 funALTVss
37057 disjss
37089 dvhopellsm
39476 diclspsn
39553 dih1dimatlem
39688 |