Theorem fovcl 7474

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111   × cxp 5612  ⟶wf 6477  (class class class)co 7346

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 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368

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 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-iun 4941  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-fv 6489  df-ov 7349

This theorem is referenced by:  addclnq  10836  mulclnq  10838  adderpq  10847  mulerpq  10848  distrnq  10852  axaddcl  11042  axmulcl  11044  xaddcl  13138  xmulcl  13172  elfzoelz  13559  cncrng  21325  addcnlem  24780  sgmcl  27083  hvaddcl  30992  hvmulcl  30993  hicl  31060  hhssabloilem  31241  rmxynorm  43021  rmxyneg  43023  rmxy1  43025  rmxy0  43026  rmxp1  43035  rmyp1  43036  rmxm1  43037  rmym1  43038  rmxluc  43039  rmyluc  43040  rmyluc2  43041  rmxdbl  43042  rmydbl  43043  rmxypos  43050  ltrmynn0  43051  ltrmxnn0  43052  lermxnn0  43053  rmxnn  43054  ltrmy  43055  rmyeq0  43056  rmyeq  43057  lermy  43058  rmynn  43059  rmynn0  43060  rmyabs  43061  jm2.24nn  43062  jm2.17a  43063  jm2.17b  43064  jm2.17c  43065  jm2.24  43066  rmygeid  43067  jm2.18  43091  jm2.19lem1  43092  jm2.19lem2  43093  jm2.19  43096  jm2.22  43098  jm2.23  43099  jm2.20nn  43100  jm2.25  43102  jm2.26a  43103  jm2.26lem3  43104  jm2.26  43105  jm2.15nn0  43106  jm2.16nn0  43107  jm2.27a  43108  jm2.27c  43110  rmydioph  43117  rmxdiophlem  43118  jm3.1lem1  43120  jm3.1  43123  expdiophlem1  43124