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 1427	1 ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝐶)

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119   × cxp 5616  ⟶wf 6481  (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 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-fv 6493  df-ov 7359

This theorem is referenced by:  addclnq  10859  mulclnq  10861  adderpq  10870  mulerpq  10871  distrnq  10875  axaddcl  11065  axmulcl  11067  xaddcl  13182  xmulcl  13216  elfzoelz  13604  cncrng  21368  addcnlem  24848  sgmcl  27127  hvaddcl  31101  hvmulcl  31102  hicl  31169  hhssabloilem  31350  rmxynorm  43363  rmxyneg  43365  rmxy1  43367  rmxy0  43368  rmxp1  43377  rmyp1  43378  rmxm1  43379  rmym1  43380  rmxluc  43381  rmyluc  43382  rmyluc2  43383  rmxdbl  43384  rmydbl  43385  rmxypos  43392  ltrmynn0  43393  ltrmxnn0  43394  lermxnn0  43395  rmxnn  43396  ltrmy  43397  rmyeq0  43398  rmyeq  43399  lermy  43400  rmynn  43401  rmynn0  43402  rmyabs  43403  jm2.24nn  43404  jm2.17a  43405  jm2.17b  43406  jm2.17c  43407  jm2.24  43408  rmygeid  43409  jm2.18  43433  jm2.19lem1  43434  jm2.19lem2  43435  jm2.19  43438  jm2.22  43440  jm2.23  43441  jm2.20nn  43442  jm2.25  43444  jm2.26a  43445  jm2.26lem3  43446  jm2.26  43447  jm2.15nn0  43448  jm2.16nn0  43449  jm2.27a  43450  jm2.27c  43452  rmydioph  43459  rmxdiophlem  43460  jm3.1lem1  43462  jm3.1  43465  expdiophlem1  43466