Theorem ovmpog 6061

Description: Value of an operation given by a maps-to rule. Special case. (Contributed by NM, 14-Sep-1999.) (Revised by David Abernethy, 19-Jun-2012.)

Hypotheses

Ref	Expression
ovmpog.1	|- ( x = A -> R = G )
ovmpog.2	|- ( y = B -> G = S )
ovmpog.3	|- F = ( x e. C , y e. D |-> R )

Assertion

Ref	Expression
ovmpog	|- ( ( A e. C /\ B e. D /\ S e. H ) -> ( A F B ) = S )

Distinct variable groups:   x, y, A   x, B, y   x, C, y   x, D, y   x, S, y

Allowed substitution hints:   R( x, y)   F( x, y)   G( x, y)   H( x, y)

Proof of Theorem ovmpog

Step	Hyp	Ref	Expression
1		ovmpog.1	. . 3 |- ( x = A -> R = G )
2		ovmpog.2	. . 3 |- ( y = B -> G = S )
3	1, 2	sylan9eq 2249	. 2 |- ( ( x = A /\ y = B ) -> R = S )
4		ovmpog.3	. 2 |- F = ( x e. C , y e. D |-> R )
5	3, 4	ovmpoga 6056	1 |- ( ( A e. C /\ B e. D /\ S e. H ) -> ( A F B ) = S )

Syntax hints:   -> wi 4   /\ w3a 980   = wceq 1364   e. wcel 2167  (class class class)co 5925   e. cmpo 5927

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-14 2170  ax-ext 2178  ax-sep 4152  ax-pow 4208  ax-pr 4243  ax-setind 4574

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1475  df-sb 1777  df-eu 2048  df-mo 2049  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ne 2368  df-ral 2480  df-rex 2481  df-v 2765  df-sbc 2990  df-dif 3159  df-un 3161  df-in 3163  df-ss 3170  df-pw 3608  df-sn 3629  df-pr 3630  df-op 3632  df-uni 3841  df-br 4035  df-opab 4096  df-id 4329  df-xp 4670  df-rel 4671  df-cnv 4672  df-co 4673  df-dm 4674  df-iota 5220  df-fun 5261  df-fv 5267  df-ov 5928  df-oprab 5929  df-mpo 5930

This theorem is referenced by:  ovmpo  6062  oav  6521  omv  6522  oeiv  6523  mapvalg  6726  pmvalg  6727  mulpipq2  7455  genipv  7593  genpelxp  7595  subval  8235  divvalap  8718  cnref1o  9742  modqval  10433  frecuzrdgrrn  10517  frec2uzrdg  10518  frecuzrdgrcl  10519  frecuzrdgsuc  10523  frecuzrdgrclt  10524  frecuzrdgg  10525  frecuzrdgsuctlem  10532  seq3val  10569  seqvalcd  10570  seqf  10573  seq3p1  10574  seqovcd  10576  seqp1cd  10579  exp3val  10650  bcval  10858  shftfvalg  11000  shftfval  11003  cnrecnv  11092  gcdval  12151  sqpweven  12368  2sqpwodd  12369  ennnfonelemp1  12648  nninfdclemcl  12690  nninfdclemp1  12692  ressvalsets  12767  imasex  13007  qusex  13027  mhmex  13164  releqgg  13426  eqgex  13427  isghm  13449  gsumfzfsumlemm  14219  cnfldui  14221  expghmap  14239  cnprcl2k  14526  xmetxp  14827  expcn  14889  cncfval  14892  dvply2g  15086  rpcxpef  15214  rplogbval  15265  mpodvdsmulf1o  15310  fsumdvdsmul  15311