Theorem opreq 4025

Description: Equality theorem for operation value.

Assertion

Ref	Expression
opreq	|- (F = G -> (AFB) = (AGB))

Proof of Theorem opreq

Step	Hyp	Ref	Expression
1		fveq1 3780	. 2 |- (F = G -> (F` <.A, B>.) = (G` <.A, B>.))
2		df-opr 4023	. 2 |- (AFB) = (F` <.A, B>.)
3		df-opr 4023	. 2 |- (AGB) = (G` <.A, B>.)
4	1, 2, 3	3eqtr4g 1578	1 |- (F = G -> (AFB) = (AGB))

Syntax hints:   -> wi 3   = wceq 997  <.cop 2463  ` cfv 3239  (class class class)co 4021

This theorem is referenced by:  opreqi 4032  opreqd 4035  hboprd 4040  mapxpen 4560  seq1val 6571  ismet 7883  ismsg 7885  msflem 7888  blfval 7920  isgrp 8126  grpidval 8142  grpinvfval 8150  grpdivfval 8165  isabl 8185  isring 8225  ringi 8226  vci 8251  isvclem 8280  isnvlem 8313  nvi 8317  isphg 8560  elghomlem1 10467  vri 10583  isded 10751  dedi 10752  iscat 10769  cati 10770  ismona 10819

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-10 1007  ax-11 1008  ax-12 1009  ax-13 1010  ax-14 1011  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504  ax-sep 2758  ax-pow 2798  ax-pr 2835

This theorem depends on definitions:  df-bi 154  df-or 231  df-an 232  df-ex 1022  df-sb 1214  df-eu 1424  df-mo 1425  df-clab 1510  df-cleq 1515  df-clel 1518  df-ne 1634  df-v 1859  df-dif 2100  df-un 2101  df-in 2102  df-ss 2104  df-nul 2332  df-pw 2454  df-sn 2464  df-pr 2465  df-op 2468  df-uni 2558  df-br 2675  df-opab 2722  df-cnv 3243  df-dm 3245  df-rn 3246  df-res 3247  df-ima 3248  df-fv 3255  df-opr 4023

Copyright terms: Public domain