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

Theorem rspceov 6283
Description: A frequently used special case of rspc2ev 3131 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 6251 . . 3  |-  ( x  =  C  ->  (
x F y )  =  ( C F y ) )
21eqeq2d 2433 . 2  |-  ( x  =  C  ->  ( S  =  ( x F y )  <->  S  =  ( C F y ) ) )
3 oveq2 6252 . . 3  |-  ( y  =  D  ->  ( C F y )  =  ( C F D ) )
43eqeq2d 2433 . 2  |-  ( y  =  D  ->  ( S  =  ( C F y )  <->  S  =  ( C F D ) ) )
52, 4rspc2ev 3131 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 982    = wceq 1437    e. wcel 1872   E.wrex 2710  (class class class)co 6244
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-rex 2715  df-rab 2718  df-v 3019  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-nul 3700  df-if 3850  df-sn 3937  df-pr 3939  df-op 3943  df-uni 4158  df-br 4362  df-iota 5503  df-fv 5547  df-ov 6247
This theorem is referenced by:  iunfictbso  8491  genpprecl  9372  elz2  10900  zaddcl  10923  znq  11214  qaddcl  11226  qmulcl  11228  qreccl  11230  xpsff1o  15412  mndpfo  16498  gafo  16888  lsmelvalix  17231  lsmelvalmi  17242  evthicc2  22348  i1fadd  22590  i1fmul  22591  isgrpoi  25863  isgrpda  25962  shscli  26907  shsva  26910  shunssi  26958  pjpjhth  27015  spanunsni  27169  pjjsi  27290  ofrn2  28182  pstmfval  28646  ismblfin  31888  itg2addnc  31903  blbnd  32026  sgoldbalt  38695
  Copyright terms: Public domain W3C validator