Theorem fovcl 7538

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2143   × cxp 5659  ⟶wf 6532  (class class class)co 7410

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-fv 6544  df-ov 7413

This theorem is referenced by:  addclnq  10925  mulclnq  10927  adderpq  10936  mulerpq  10937  distrnq  10941  axaddcl  11131  axmulcl  11133  xaddcl  13260  xmulcl  13294  elfzoelz  13683  cncrng  21543  addcnlem  25022  sgmcl  27310  hvaddcl  31364  hvmulcl  31365  hicl  31432  hhssabloilem  31613  rmxynorm  43665  rmxyneg  43667  rmxy1  43669  rmxy0  43670  rmxp1  43679  rmyp1  43680  rmxm1  43681  rmym1  43682  rmxluc  43683  rmyluc  43684  rmyluc2  43685  rmxdbl  43686  rmydbl  43687  rmxypos  43694  ltrmynn0  43695  ltrmxnn0  43696  lermxnn0  43697  rmxnn  43698  ltrmy  43699  rmyeq0  43700  rmyeq  43701  lermy  43702  rmynn  43703  rmynn0  43704  rmyabs  43705  jm2.24nn  43706  jm2.17a  43707  jm2.17b  43708  jm2.17c  43709  jm2.24  43710  rmygeid  43711  jm2.18  43735  jm2.19lem1  43736  jm2.19lem2  43737  jm2.19  43740  jm2.22  43742  jm2.23  43743  jm2.20nn  43744  jm2.25  43746  jm2.26a  43747  jm2.26lem3  43748  jm2.26  43749  jm2.15nn0  43750  jm2.16nn0  43751  jm2.27a  43752  jm2.27c  43754  rmydioph  43761  rmxdiophlem  43762  jm3.1lem1  43764  jm3.1  43767  expdiophlem1  43768