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
12996 dflt2
12997 isinv
17579 invsym2
17582 invfun
17583 oppcsect2
17598 oppcinv
17599 relfull
17731 relfth
17732 psss
18405 gicer
19001 gsum2d
19684 isunit
20015 txdis1cn
22914 hmpher
23063 tgphaus
23396 qustgplem
23400 tsmsxp
23434 xmeter
23714 ovoliunlem1
24794 taylf
25648 lgsquadlem1
26656 lgsquadlem2
26657 nvrel
29349 phrel
29562 bnrel
29614 hlrel
29637 gonan0
33766 frxp2
34183 frxp3
34189 sscoid
34429 trer
34719 fneer
34756 heicant
36044 iss2
36736 funALTVss
37092 disjss
37124 dvhopellsm
39511 diclspsn
39588 dih1dimatlem
39723 |