Theorem ovrspc2v 7434

Description: If an operation value is element of a class for all operands of two classes, then the operation value is an element of the class for specific operands of the two classes. (Contributed by Mario Carneiro, 6-Dec-2014.)

Assertion

Ref	Expression
ovrspc2v	⊢ (((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝐹𝑦) ∈ 𝐶) → (𝑋𝐹𝑌) ∈ 𝐶)

Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝑥,𝐶,𝑦   𝑥,𝐹,𝑦   𝑦,𝑌   𝑥,𝑋,𝑦

Allowed substitution hint:   𝑌(𝑥)

Proof of Theorem ovrspc2v

Step	Hyp	Ref	Expression
1		oveq1 7415	. . 3 ⊢ (𝑥 = 𝑋 → (𝑥𝐹𝑦) = (𝑋𝐹𝑦))
2	1	eleq1d 2818	. 2 ⊢ (𝑥 = 𝑋 → ((𝑥𝐹𝑦) ∈ 𝐶 ↔ (𝑋𝐹𝑦) ∈ 𝐶))
3		oveq2 7416	. . 3 ⊢ (𝑦 = 𝑌 → (𝑋𝐹𝑦) = (𝑋𝐹𝑌))
4	3	eleq1d 2818	. 2 ⊢ (𝑦 = 𝑌 → ((𝑋𝐹𝑦) ∈ 𝐶 ↔ (𝑋𝐹𝑌) ∈ 𝐶))
5	2, 4	rspc2va 3623	1 ⊢ (((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝐹𝑦) ∈ 𝐶) → (𝑋𝐹𝑌) ∈ 𝐶)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  ∀wral 3061  (class class class)co 7408

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551  df-ov 7411

This theorem is referenced by:  off  7687  mgmcl  18563  sgrppropd  18621  mndpropd  18649  issubmnd  18651  submcl  18692  issubg2  19020  gass  19164  lmodprop2d  20533  lsspropd  20627  gsummatr01lem2  22157  off2  31861  ofcf  33096  fsuppind  41164  submgmcl  46554  clcllaw  46591