![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > ovprc1 | Structured 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 457 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | con3i 135 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | ovprc1.1 |
. . 3
![]() ![]() ![]() ![]() | |
4 | 3 | ovprc 6219 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | syl 16 |
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 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1952 ax-ext 2430 ax-sep 4513 ax-nul 4521 ax-pow 4570 ax-pr 4631 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2264 df-mo 2265 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2601 df-ne 2646 df-ral 2800 df-rex 2801 df-rab 2804 df-v 3072 df-dif 3431 df-un 3433 df-in 3435 df-ss 3442 df-nul 3738 df-if 3892 df-sn 3978 df-pr 3980 df-op 3984 df-uni 4192 df-br 4393 df-opab 4451 df-xp 4946 df-rel 4947 df-dm 4950 df-iota 5481 df-fv 5526 df-ov 6195 |
This theorem is referenced by: mapdom2 7584 setsnid 14320 ressbas 14332 resslem 14335 ressinbas 14338 ressress 14339 oduval 15404 oduleval 15405 gsum0 15614 oppgval 15966 oppgplusfval 15967 mgpval 16701 opprval 16824 srasca 17370 rlmsca2 17390 resspsrbas 17596 mplrcl 17680 mpfrcl 17713 psrbaspropd 17798 mplbaspropd 17800 strov2rcl 17801 evl1fval1 17876 dsmmval 18270 dsmmbas2 18273 dsmmfi 18274 qtopres 19389 fgabs 19570 tnglem 20344 tngds 20352 tchval 20851 resvsca 26434 resvlem 26435 mapco2g 29190 mzpmfp 29223 mzpmfpOLD 29224 mendbas 29681 |
Copyright terms: Public domain | W3C validator |