Theorem rspceov 7454

Description: A frequently used special case of rspc2ev 3614 for operation values. (Contributed by NM, 21-Mar-2007.)

Assertion

Ref	Expression
rspceov	⊢ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ∧ 𝑆 = (𝐶𝐹𝐷)) → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑆 = (𝑥𝐹𝑦))

Distinct variable groups:   𝑥,𝐴   𝑥,𝑦,𝐵   𝑥,𝐶,𝑦   𝑦,𝐷   𝑥,𝐹,𝑦   𝑥,𝑆,𝑦

Allowed substitution hints:   𝐴(𝑦)   𝐷(𝑥)

Proof of Theorem rspceov

Step	Hyp	Ref	Expression
1		oveq1 7412	. . 3 ⊢ (𝑥 = 𝐶 → (𝑥𝐹𝑦) = (𝐶𝐹𝑦))
2	1	eqeq2d 2746	. 2 ⊢ (𝑥 = 𝐶 → (𝑆 = (𝑥𝐹𝑦) ↔ 𝑆 = (𝐶𝐹𝑦)))
3		oveq2 7413	. . 3 ⊢ (𝑦 = 𝐷 → (𝐶𝐹𝑦) = (𝐶𝐹𝐷))
4	3	eqeq2d 2746	. 2 ⊢ (𝑦 = 𝐷 → (𝑆 = (𝐶𝐹𝑦) ↔ 𝑆 = (𝐶𝐹𝐷)))
5	2, 4	rspc2ev 3614	1 ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ∧ 𝑆 = (𝐶𝐹𝐷)) → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑆 = (𝑥𝐹𝑦))

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2108  ∃wrex 3060  (class class class)co 7405

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6484  df-fv 6539  df-ov 7408

This theorem is referenced by:  iunfictbso  10128  genpprecl  11015  elz2  12606  zaddcl  12632  znq  12968  qaddcl  12981  qmulcl  12983  qreccl  12985  xpsff1o  17581  mndpfo  18735  gafo  19279  lsmelvalix  19622  lsmelvalmi  19633  evthicc2  25413  i1fadd  25648  i1fmul  25649  nnzsubs  28325  nnzs  28326  0zs  28328  zmulscld  28337  elzn0s  28338  2clwwlk2clwwlk  30331  isgrpoi  30479  shscli  31298  shsva  31301  shunssi  31349  pjpjhth  31406  spanunsni  31560  pjjsi  31681  ofrn2  32618  elringlsmd  33409  pstmfval  33927  ismblfin  37685  itg2addnc  37698  blbnd  37811  isgrpda  37979  sbgoldbalt  47795