Theorem fovcl 7498

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114   × cxp 5632  ⟶wf 6498  (class class class)co 7370

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5245  ax-nul 5255  ax-pr 5381

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5529  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-iota 6458  df-fun 6504  df-fn 6505  df-f 6506  df-fv 6510  df-ov 7373

This theorem is referenced by:  addclnq  10870  mulclnq  10872  adderpq  10881  mulerpq  10882  distrnq  10886  axaddcl  11076  axmulcl  11078  xaddcl  13168  xmulcl  13202  elfzoelz  13589  cncrng  21360  addcnlem  24826  sgmcl  27129  hvaddcl  31106  hvmulcl  31107  hicl  31174  hhssabloilem  31355  rmxynorm  43304  rmxyneg  43306  rmxy1  43308  rmxy0  43309  rmxp1  43318  rmyp1  43319  rmxm1  43320  rmym1  43321  rmxluc  43322  rmyluc  43323  rmyluc2  43324  rmxdbl  43325  rmydbl  43326  rmxypos  43333  ltrmynn0  43334  ltrmxnn0  43335  lermxnn0  43336  rmxnn  43337  ltrmy  43338  rmyeq0  43339  rmyeq  43340  lermy  43341  rmynn  43342  rmynn0  43343  rmyabs  43344  jm2.24nn  43345  jm2.17a  43346  jm2.17b  43347  jm2.17c  43348  jm2.24  43349  rmygeid  43350  jm2.18  43374  jm2.19lem1  43375  jm2.19lem2  43376  jm2.19  43379  jm2.22  43381  jm2.23  43382  jm2.20nn  43383  jm2.25  43385  jm2.26a  43386  jm2.26lem3  43387  jm2.26  43388  jm2.15nn0  43389  jm2.16nn0  43390  jm2.27a  43391  jm2.27c  43393  rmydioph  43400  rmxdiophlem  43401  jm3.1lem1  43403  jm3.1  43406  expdiophlem1  43407