Theorem fovcl 7529

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2098   × cxp 5664  ⟶wf 6529  (class class class)co 7401

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5289  ax-nul 5296  ax-pr 5417

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-nul 4315  df-if 4521  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-id 5564  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-fv 6541  df-ov 7404

This theorem is referenced by:  addclnq  10936  mulclnq  10938  adderpq  10947  mulerpq  10948  distrnq  10952  axaddcl  11142  axmulcl  11144  xaddcl  13215  xmulcl  13249  elfzoelz  13629  addcnlem  24702  sgmcl  26994  hvaddcl  30734  hvmulcl  30735  hicl  30802  hhssabloilem  30983  gg-cncrng  35673  rmxynorm  42146  rmxyneg  42148  rmxy1  42150  rmxy0  42151  rmxp1  42160  rmyp1  42161  rmxm1  42162  rmym1  42163  rmxluc  42164  rmyluc  42165  rmyluc2  42166  rmxdbl  42167  rmydbl  42168  rmxypos  42175  ltrmynn0  42176  ltrmxnn0  42177  lermxnn0  42178  rmxnn  42179  ltrmy  42180  rmyeq0  42181  rmyeq  42182  lermy  42183  rmynn  42184  rmynn0  42185  rmyabs  42186  jm2.24nn  42187  jm2.17a  42188  jm2.17b  42189  jm2.17c  42190  jm2.24  42191  rmygeid  42192  jm2.18  42216  jm2.19lem1  42217  jm2.19lem2  42218  jm2.19  42221  jm2.22  42223  jm2.23  42224  jm2.20nn  42225  jm2.25  42227  jm2.26a  42228  jm2.26lem3  42229  jm2.26  42230  jm2.15nn0  42231  jm2.16nn0  42232  jm2.27a  42233  jm2.27c  42235  rmydioph  42242  rmxdiophlem  42243  jm3.1lem1  42245  jm3.1  42248  expdiophlem1  42249