![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ovprc1 | Structured version Visualization version Unicode version |
Description: The value of an operation when the first argument is a proper class. (Contributed by NM, 16-Jun-2004.) |
Ref | Expression |
---|---|
ovprc1.1 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
ovprc1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl 463 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | con3i 142 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | ovprc1.1 |
. . 3
![]() ![]() ![]() ![]() | |
4 | 3 | ovprc 6345 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | syl 17 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-8 1900 ax-9 1907 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 ax-sep 4539 ax-nul 4548 ax-pow 4595 ax-pr 4653 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3an 993 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-eu 2314 df-mo 2315 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-ne 2635 df-ral 2754 df-rex 2755 df-rab 2758 df-v 3059 df-dif 3419 df-un 3421 df-in 3423 df-ss 3430 df-nul 3744 df-if 3894 df-sn 3981 df-pr 3983 df-op 3987 df-uni 4213 df-br 4417 df-opab 4476 df-xp 4859 df-rel 4860 df-dm 4863 df-iota 5565 df-fv 5609 df-ov 6318 |
This theorem is referenced by: mapdom2 7769 setsnid 15214 ressbas 15228 resslem 15231 ressinbas 15234 ressress 15236 oduval 16425 oduleval 16426 gsum0 16570 oppgval 17047 oppgplusfval 17048 mgpval 17775 opprval 17901 srasca 18453 rlmsca2 18473 resspsrbas 18688 mpfrcl 18790 psrbaspropd 18877 mplbaspropd 18879 evl1fval1 18968 dsmmval 19346 dsmmbas2 19349 dsmmfi 19350 qtopres 20762 fgabs 20943 tnglem 21697 tngds 21705 tchval 22241 resvsca 28642 resvlem 28643 mapco2g 35601 mzpmfp 35634 mendbas 36095 |
Copyright terms: Public domain | W3C validator |