Theorem fovcl 7561

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108   × cxp 5683  ⟶wf 6557  (class class class)co 7431

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-fv 6569  df-ov 7434

This theorem is referenced by:  addclnq  10985  mulclnq  10987  adderpq  10996  mulerpq  10997  distrnq  11001  axaddcl  11191  axmulcl  11193  xaddcl  13281  xmulcl  13315  elfzoelz  13699  cncrng  21401  addcnlem  24886  sgmcl  27189  hvaddcl  31031  hvmulcl  31032  hicl  31099  hhssabloilem  31280  rmxynorm  42930  rmxyneg  42932  rmxy1  42934  rmxy0  42935  rmxp1  42944  rmyp1  42945  rmxm1  42946  rmym1  42947  rmxluc  42948  rmyluc  42949  rmyluc2  42950  rmxdbl  42951  rmydbl  42952  rmxypos  42959  ltrmynn0  42960  ltrmxnn0  42961  lermxnn0  42962  rmxnn  42963  ltrmy  42964  rmyeq0  42965  rmyeq  42966  lermy  42967  rmynn  42968  rmynn0  42969  rmyabs  42970  jm2.24nn  42971  jm2.17a  42972  jm2.17b  42973  jm2.17c  42974  jm2.24  42975  rmygeid  42976  jm2.18  43000  jm2.19lem1  43001  jm2.19lem2  43002  jm2.19  43005  jm2.22  43007  jm2.23  43008  jm2.20nn  43009  jm2.25  43011  jm2.26a  43012  jm2.26lem3  43013  jm2.26  43014  jm2.15nn0  43015  jm2.16nn0  43016  jm2.27a  43017  jm2.27c  43019  rmydioph  43026  rmxdiophlem  43027  jm3.1lem1  43029  jm3.1  43032  expdiophlem1  43033