Colors of
variables: wff
setvar class |
Syntax hints:
⊆ wss 3943 ⟨cop 4629
∪ cuni 4902
ran crn 5670 ‘cfv 6537
(class class class)co 7405 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905
ax-6 1963 ax-7 2003 ax-8 2100
ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2163 ax-ext 2697 ax-sep 5292 ax-nul 5299 ax-pr 5420 |
This theorem depends on definitions:
df-bi 206 df-an 396
df-or 845 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2704 df-cleq 2718 df-clel 2804 df-ne 2935 df-ral 3056 df-rex 3065 df-rab 3427 df-v 3470 df-dif 3946 df-un 3948 df-in 3950 df-ss 3960 df-nul 4318 df-if 4524 df-sn 4624 df-pr 4626 df-op 4630 df-uni 4903 df-br 5142 df-opab 5204 df-cnv 5677 df-dm 5679 df-rn 5680 df-iota 6489 df-fv 6545 df-ov 7408 |
This theorem is referenced by: prdsvallem
17409 prdsplusg
17413 prdsmulr
17414 prdsvsca
17415 prdshom
17422 wunfunc
17860 wunfuncOLD
17861 wunnat
17919 wunnatOLD
17920 homarw
18008 catcoppccl
18079 catcoppcclOLD
18080 catcfuccl
18081 catcfucclOLD
18082 catcxpccl
18171 catcxpcclOLD
18172 isanmbfmOLD
33783 isanmbfm
33785 |