Theorem fovcl 7560

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 7559	. 2 ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝐶)
4	3	3anidm12 1418	1 ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105   × cxp 5686  ⟶wf 6558  (class class class)co 7430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-fv 6570  df-ov 7433

This theorem is referenced by:  addclnq  10982  mulclnq  10984  adderpq  10993  mulerpq  10994  distrnq  10998  axaddcl  11188  axmulcl  11190  xaddcl  13277  xmulcl  13311  elfzoelz  13695  cncrng  21418  addcnlem  24899  sgmcl  27203  hvaddcl  31040  hvmulcl  31041  hicl  31108  hhssabloilem  31289  rmxynorm  42906  rmxyneg  42908  rmxy1  42910  rmxy0  42911  rmxp1  42920  rmyp1  42921  rmxm1  42922  rmym1  42923  rmxluc  42924  rmyluc  42925  rmyluc2  42926  rmxdbl  42927  rmydbl  42928  rmxypos  42935  ltrmynn0  42936  ltrmxnn0  42937  lermxnn0  42938  rmxnn  42939  ltrmy  42940  rmyeq0  42941  rmyeq  42942  lermy  42943  rmynn  42944  rmynn0  42945  rmyabs  42946  jm2.24nn  42947  jm2.17a  42948  jm2.17b  42949  jm2.17c  42950  jm2.24  42951  rmygeid  42952  jm2.18  42976  jm2.19lem1  42977  jm2.19lem2  42978  jm2.19  42981  jm2.22  42983  jm2.23  42984  jm2.20nn  42985  jm2.25  42987  jm2.26a  42988  jm2.26lem3  42989  jm2.26  42990  jm2.15nn0  42991  jm2.16nn0  42992  jm2.27a  42993  jm2.27c  42995  rmydioph  43002  rmxdiophlem  43003  jm3.1lem1  43005  jm3.1  43008  expdiophlem1  43009