opreqd - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem opreqd 4899

Description: Equality deduction for operation value.

**Hypothesis**
Ref	Expression
opreq1d.1

**Assertion**
Ref	Expression
opreqd

**Proof of Theorem opreqd**
Step	Hyp	Ref	Expression
1		opreq1d.1	. 2
2		opreq 4888	. 2
3	1, 2	syl 12	1

Colors of variables: wff set class

Syntax hints:

wi 3

wceq 1298 (class class class)co 4884

This theorem is referenced by: csboprgOLD 4911 csbopr12g 4912 oprssoprv 4964 blval 9114 metcnss 9176 metcnss2 9177 grpdivval 9367 gxval 9381 subgopr 9427 vcoprne 9530 vacn 9673 ipfval 9691 ipval 9692 sspgval 9727 sspsval 9729 lnoval 9752 ajfval 9809 ipdir 9843 ipass 9846 opreq123d 10153 oprssoprvg 14335 ismona 15158 isepia 15168 cinvlem1 15176 isfuna 15182 istotbnd 15933 isbnd 15939 rrnmval 16014 phtpyval 16047 phtpcval 16058 pcoval 16073 pi1fval 16092 pi1val 16094 rnghomval 16118 idlval 16161 pridlval 16181 joinval 16815 meetval 16822 islat 16849 isopos 16909 cmtfval 16937 ishlat 17018 grpidvalNEW 17117 grpinvfvalNEW 17125 isablNEW 17135 ringidval 17149 plusssfval 17204 plusssval 17205 ocvfval 17206 ishil 17210 lineset 17219 psubspset 17225 paddfval 17258 paddval 17259 trnfset 17404

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 1304 ax-gen 1305 ax-8 1306 ax-9 1307 ax-10 1308 ax-11 1309 ax-12 1310 ax-14 1312 ax-17 1317 ax-4 1319 ax-5o 1321 ax-6o 1324 ax-9o 1481 ax-10o 1500 ax-16 1580 ax-11o 1588 ax-ext 1865 ax-sep 3438 ax-nul 3445 ax-pow 3481 ax-pr 3524

This theorem depends on definitions: df-bi 164 df-or 241 df-an 242 df-ex 1327 df-sb 1536 df-eu 1775 df-mo 1776 df-clab 1872 df-cleq 1877 df-clel 1880 df-ne 2019 df-rex 2110 df-v 2294 df-dif 2597 df-un 2600 df-in 2603 df-ss 2605 df-nul 2876 df-pw 3035 df-sn 3049 df-pr 3050 df-op 3053 df-uni 3178 df-br 3339 df-opab 3396 df-cnv 4002 df-dm 4004 df-rn 4005 df-res 4006 df-ima 4007 df-fv 4014 df-opr 4886