Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 = wceq 1542
∈ wcel 2107 ×
cxp 5636 ↾ cres 5640
(class class class)co 7362 |
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 2708 ax-sep 5261 ax-nul 5268 ax-pr 5389 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-ral 3066 df-rex 3075 df-rab 3411 df-v 3450 df-dif 3918 df-un 3920 df-in 3922 df-ss 3932 df-nul 4288 df-if 4492 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4871 df-br 5111 df-opab 5173 df-xp 5644 df-res 5650 df-iota 6453 df-fv 6509 df-ov 7365 |
This theorem is referenced by: sscres
17713 fullsubc
17743 fullresc
17744 funcres2c
17795 psmetres2
23683 xmetres2
23730 prdsdsf
23736 xpsdsval
23750 xmssym
23834 xmstri2
23835 mstri2
23836 xmstri
23837 mstri
23838 xmstri3
23839 mstri3
23840 msrtri
23841 tmsxpsval
23910 ngptgp
24008 nlmvscn
24067 nrginvrcn
24072 nghmcn
24125 cnmpt1ds
24221 cnmpt2ds
24222 ipcn
24626 caussi
24677 causs
24678 minveclem2
24806 minveclem3b
24808 minveclem3
24809 minveclem4
24812 minveclem6
24814 ftc1lem6
25421 ulmdvlem1
25775 abelth
25816 cxpcn3
26117 rlimcnp
26331 hhssnv
30248 madjusmdetlem3
32450 qqhcn
32612 qqhucn
32613 ftc1cnnc
36179 ismtyres
36296 isdrngo2
36446 naddcnffo
41709 rngchom
46339 ringchom
46385 irinitoringc
46441 rhmsubclem4
46461 |