Theorem rspceov 7461

Description: A frequently used special case of rspc2ev 3589 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 7419	. . 3 ⊢ (𝑥 = 𝐶 → (𝑥𝐹𝑦) = (𝐶𝐹𝑦))
2	1	eqeq2d 2772	. 2 ⊢ (𝑥 = 𝐶 → (𝑆 = (𝑥𝐹𝑦) ↔ 𝑆 = (𝐶𝐹𝑦)))
3		oveq2 7420	. . 3 ⊢ (𝑦 = 𝐷 → (𝐶𝐹𝑦) = (𝐶𝐹𝐷))
4	3	eqeq2d 2772	. 2 ⊢ (𝑦 = 𝐷 → (𝑆 = (𝐶𝐹𝑦) ↔ 𝑆 = (𝐶𝐹𝐷)))
5	2, 4	rspc2ev 3589	1 ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ∧ 𝑆 = (𝐶𝐹𝐷)) → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑆 = (𝑥𝐹𝑦))

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  ∃wrex 3087  (class class class)co 7412

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6487  df-fv 6539  df-ov 7415

This theorem is used by:  iunfictbso  10174  genpprecl  11067  elz2  12692  zaddcl  12717  znq  13060  qaddcl  13074  qmulcl  13076  qreccl  13078  xpsff1o  17719  mndpfoOLD  18929  gafo  19490  lsmelvalix  19835  lsmelvalmi  19846  elmgplsmd  20353  evthicc2  25761  i1fadd  25996  i1fmul  25997  nnzsubs  28753  nnzs  28754  0zs  28756  zmulscld  28765  elzn0s  28766  2clwwlk2clwwlk  30933  isgrpoi  31082  shscli  31901  shsva  31904  shunssi  31952  pjpjhth  32009  spanunsni  32163  pjjsi  32284  ofrn2  33216  pstmfval  34510  ismblfin  38547  itg2addnc  38560  blbnd  38689  isgrpda  38857  sbgoldbalt  48823