Theorem fovcl 7484

Description: Closure law for an operation. (Contributed by NM, 19-Apr-2007.) (Proof shortened by AV, 9-Mar-2025.)

Hypothesis

Ref	Expression
fovcl.1	⊢ 𝐹:(𝑅 × 𝑆)⟶𝐶

Assertion

Ref	Expression
fovcl	⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝐶)

Proof of Theorem fovcl

Step	Hyp	Ref	Expression
1		fovcl.1	. . . 4 ⊢ 𝐹:(𝑅 × 𝑆)⟶𝐶
2	1	a1i 11	. . 3 ⊢ (𝐴 ∈ 𝑅 → 𝐹:(𝑅 × 𝑆)⟶𝐶)
3	2	fovcld 7483	. 2 ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝐶)
4	3	3anidm12 1421	1 ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113   × cxp 5620  ⟶wf 6486  (class class class)co 7356

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-iun 4946  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-fv 6498  df-ov 7359

This theorem is referenced by:  addclnq  10854  mulclnq  10856  adderpq  10865  mulerpq  10866  distrnq  10870  axaddcl  11060  axmulcl  11062  xaddcl  13152  xmulcl  13186  elfzoelz  13573  cncrng  21341  addcnlem  24807  sgmcl  27110  hvaddcl  31036  hvmulcl  31037  hicl  31104  hhssabloilem  31285  rmxynorm  43102  rmxyneg  43104  rmxy1  43106  rmxy0  43107  rmxp1  43116  rmyp1  43117  rmxm1  43118  rmym1  43119  rmxluc  43120  rmyluc  43121  rmyluc2  43122  rmxdbl  43123  rmydbl  43124  rmxypos  43131  ltrmynn0  43132  ltrmxnn0  43133  lermxnn0  43134  rmxnn  43135  ltrmy  43136  rmyeq0  43137  rmyeq  43138  lermy  43139  rmynn  43140  rmynn0  43141  rmyabs  43142  jm2.24nn  43143  jm2.17a  43144  jm2.17b  43145  jm2.17c  43146  jm2.24  43147  rmygeid  43148  jm2.18  43172  jm2.19lem1  43173  jm2.19lem2  43174  jm2.19  43177  jm2.22  43179  jm2.23  43180  jm2.20nn  43181  jm2.25  43183  jm2.26a  43184  jm2.26lem3  43185  jm2.26  43186  jm2.15nn0  43187  jm2.16nn0  43188  jm2.27a  43189  jm2.27c  43191  rmydioph  43198  rmxdiophlem  43199  jm3.1lem1  43201  jm3.1  43204  expdiophlem1  43205