Theorem oprvalres 4091

Description: The value of a restricted operation. (Contributed by FL, 10-Nov-2006.)

Assertion

Ref	Expression
oprvalres	|- ((A e. C /\ B e. D) -> (A(F |` (C X. D))B) = (AFB))

Proof of Theorem oprvalres

Step	Hyp	Ref	Expression
1		opelxpi 3274	. . 3 |- ((A e. C /\ B e. D) -> <.A, B>. e. (C X. D))
2		fvres 3791	. . 3 |- (<.A, B>. e. (C X. D) -> ((F |` (C X. D))` <.A, B>.) = (F` <.A, B>.))
3	1, 2	syl 10	. 2 |- ((A e. C /\ B e. D) -> ((F |` (C X. D))` <.A, B>.) = (F` <.A, B>.))
4		df-opr 4023	. 2 |- (A(F |` (C X. D))B) = ((F |` (C X. D))` <.A, B>.)
5		df-opr 4023	. 2 |- (AFB) = (F` <.A, B>.)
6	3, 4, 5	3eqtr4g 1578	1 |- ((A e. C /\ B e. D) -> (A(F |` (C X. D))B) = (AFB))

Syntax hints:   -> wi 3   /\ wa 230   = wceq 997   e. wcel 999  <.cop 2463   X. cxp 3225   |` cres 3229  ` cfv 3239  (class class class)co 4021

This theorem is referenced by:  oprssoprval 4092  mulnzcnopr 5767  metreslem 7907  metcnss 7983  metcnss2 7984  cncfmet 7990  lmss 8038  caussi 8039  causs 8040  subgopr 8202  issubgi 8206  ablmul 8215  mulid 8216  ghgrpilem1 8217  sspgval 8472  sspsval 8474  sspmlem 8475  shftefif1olem 8824  hhssabli 9215  hhssnv 9217  hhssmetdval 9232

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-xp 3241  df-rel 3242  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