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

Theorem rspceov 6055
Description: A frequently used special case of rspc2ev 3003 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 6027 . . 3  |-  ( x  =  C  ->  (
x F y )  =  ( C F y ) )
21eqeq2d 2398 . 2  |-  ( x  =  C  ->  ( S  =  ( x F y )  <->  S  =  ( C F y ) ) )
3 oveq2 6028 . . 3  |-  ( y  =  D  ->  ( C F y )  =  ( C F D ) )
43eqeq2d 2398 . 2  |-  ( y  =  D  ->  ( S  =  ( C F y )  <->  S  =  ( C F D ) ) )
52, 4rspc2ev 3003 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 set class
Syntax hints:    -> wi 4    /\ w3a 936    = wceq 1649    e. wcel 1717   E.wrex 2650  (class class class)co 6020
This theorem is referenced by:  iunfictbso  7928  genpprecl  8811  elz2  10230  zaddcl  10249  znq  10510  qaddcl  10522  qmulcl  10524  qreccl  10526  xpsff1o  13720  mndfo  14647  gafo  15000  lsmelvalix  15202  lsmelvalmi  15213  evthicc2  19224  i1fadd  19454  i1fmul  19455  isgrpoi  21634  isgrpda  21733  shscli  22667  shsva  22670  shunssi  22718  pjpjhth  22775  spanunsni  22929  pjjsi  23050  ofrn2  23896  blbnd  26187
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-rex 2655  df-rab 2658  df-v 2901  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-nul 3572  df-if 3683  df-sn 3763  df-pr 3764  df-op 3766  df-uni 3958  df-br 4154  df-iota 5358  df-fv 5402  df-ov 6023
  Copyright terms: Public domain W3C validator