MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rspceov Structured version   Unicode version

Theorem rspceov 6314
Description: A frequently used special case of rspc2ev 3220 for operation values. (Contributed by NM, 21-Mar-2007.)
Assertion
Ref Expression
rspceov  |-  ( ( C  e.  A  /\  D  e.  B  /\  S  =  ( C F D ) )  ->  E. x  e.  A  E. y  e.  B  S  =  ( x F y ) )
Distinct variable groups:    x, A    x, y, B    x, C, y    y, D    x, F, y    x, S, y
Allowed substitution hints:    A( y)    D( x)

Proof of Theorem rspceov
StepHypRef Expression
1 oveq1 6284 . . 3  |-  ( x  =  C  ->  (
x F y )  =  ( C F y ) )
21eqeq2d 2476 . 2  |-  ( x  =  C  ->  ( S  =  ( x F y )  <->  S  =  ( C F y ) ) )
3 oveq2 6285 . . 3  |-  ( y  =  D  ->  ( C F y )  =  ( C F D ) )
43eqeq2d 2476 . 2  |-  ( y  =  D  ->  ( S  =  ( C F y )  <->  S  =  ( C F D ) ) )
52, 4rspc2ev 3220 1  |-  ( ( C  e.  A  /\  D  e.  B  /\  S  =  ( C F D ) )  ->  E. x  e.  A  E. y  e.  B  S  =  ( x F y ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 968    = wceq 1374    e. wcel 1762   E.wrex 2810  (class class class)co 6277
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-rex 2815  df-rab 2818  df-v 3110  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3781  df-if 3935  df-sn 4023  df-pr 4025  df-op 4029  df-uni 4241  df-br 4443  df-iota 5544  df-fv 5589  df-ov 6280
This theorem is referenced by:  iunfictbso  8486  genpprecl  9370  elz2  10872  zaddcl  10894  znq  11177  qaddcl  11189  qmulcl  11191  qreccl  11193  xpsff1o  14814  mndfo  15753  gafo  16124  lsmelvalix  16452  lsmelvalmi  16463  evthicc2  21602  i1fadd  21832  i1fmul  21833  isgrpoi  24864  isgrpda  24963  shscli  25899  shsva  25902  shunssi  25950  pjpjhth  26007  spanunsni  26161  pjjsi  26282  ofrn2  27141  ismblfin  29621  itg2addnc  29635  blbnd  29875
  Copyright terms: Public domain W3C validator