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

Theorem rspceov 6317
Description: A frequently used special case of rspc2ev 3171 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 6285 . . 3  |-  ( x  =  C  ->  (
x F y )  =  ( C F y ) )
21eqeq2d 2416 . 2  |-  ( x  =  C  ->  ( S  =  ( x F y )  <->  S  =  ( C F y ) ) )
3 oveq2 6286 . . 3  |-  ( y  =  D  ->  ( C F y )  =  ( C F D ) )
43eqeq2d 2416 . 2  |-  ( y  =  D  ->  ( S  =  ( C F y )  <->  S  =  ( C F D ) ) )
52, 4rspc2ev 3171 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 974    = wceq 1405    e. wcel 1842   E.wrex 2755  (class class class)co 6278
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-rex 2760  df-rab 2763  df-v 3061  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-nul 3739  df-if 3886  df-sn 3973  df-pr 3975  df-op 3979  df-uni 4192  df-br 4396  df-iota 5533  df-fv 5577  df-ov 6281
This theorem is referenced by:  iunfictbso  8527  genpprecl  9409  elz2  10922  zaddcl  10945  znq  11231  qaddcl  11243  qmulcl  11245  qreccl  11247  xpsff1o  15182  mndpfo  16268  gafo  16658  lsmelvalix  16985  lsmelvalmi  16996  evthicc2  22164  i1fadd  22394  i1fmul  22395  isgrpoi  25614  isgrpda  25713  shscli  26649  shsva  26652  shunssi  26700  pjpjhth  26757  spanunsni  26911  pjjsi  27032  ofrn2  27923  pstmfval  28328  ismblfin  31427  itg2addnc  31442  blbnd  31565  sgoldbalt  37835
  Copyright terms: Public domain W3C validator