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

Theorem rspceov 7186
 Description: A frequently used special case of rspc2ev 3586 for operation values. (Contributed by NM, 21-Mar-2007.)
Assertion
Ref Expression
rspceov ((𝐶𝐴𝐷𝐵𝑆 = (𝐶𝐹𝐷)) → ∃𝑥𝐴𝑦𝐵 𝑆 = (𝑥𝐹𝑦))
Distinct variable groups:   𝑥,𝐴   𝑥,𝑦,𝐵   𝑥,𝐶,𝑦   𝑦,𝐷   𝑥,𝐹,𝑦   𝑥,𝑆,𝑦
Allowed substitution hints:   𝐴(𝑦)   𝐷(𝑥)

Proof of Theorem rspceov
StepHypRef Expression
1 oveq1 7146 . . 3 (𝑥 = 𝐶 → (𝑥𝐹𝑦) = (𝐶𝐹𝑦))
21eqeq2d 2812 . 2 (𝑥 = 𝐶 → (𝑆 = (𝑥𝐹𝑦) ↔ 𝑆 = (𝐶𝐹𝑦)))
3 oveq2 7147 . . 3 (𝑦 = 𝐷 → (𝐶𝐹𝑦) = (𝐶𝐹𝐷))
43eqeq2d 2812 . 2 (𝑦 = 𝐷 → (𝑆 = (𝐶𝐹𝑦) ↔ 𝑆 = (𝐶𝐹𝐷)))
52, 4rspc2ev 3586 1 ((𝐶𝐴𝐷𝐵𝑆 = (𝐶𝐹𝐷)) → ∃𝑥𝐴𝑦𝐵 𝑆 = (𝑥𝐹𝑦))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ w3a 1084   = wceq 1538   ∈ wcel 2112  ∃wrex 3110  (class class class)co 7139 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-ral 3114  df-rex 3115  df-v 3446  df-un 3889  df-in 3891  df-ss 3901  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-iota 6287  df-fv 6336  df-ov 7142 This theorem is referenced by:  iunfictbso  9529  genpprecl  10416  elz2  11991  zaddcl  12014  znq  12344  qaddcl  12356  qmulcl  12358  qreccl  12360  xpsff1o  16836  mndpfo  17930  gafo  18422  lsmelvalix  18762  lsmelvalmi  18773  evthicc2  24068  i1fadd  24303  i1fmul  24304  2clwwlk2clwwlk  28139  isgrpoi  28285  shscli  29104  shsva  29107  shunssi  29155  pjpjhth  29212  spanunsni  29366  pjjsi  29487  ofrn2  30405  elringlsmd  31005  pstmfval  31253  ismblfin  35097  itg2addnc  35110  blbnd  35224  isgrpda  35392  sbgoldbalt  44292
 Copyright terms: Public domain W3C validator