Theorem fovcl 7496

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114   × cxp 5630  ⟶wf 6496  (class class class)co 7368

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-fv 6508  df-ov 7371

This theorem is referenced by:  addclnq  10868  mulclnq  10870  adderpq  10879  mulerpq  10880  distrnq  10884  axaddcl  11074  axmulcl  11076  xaddcl  13166  xmulcl  13200  elfzoelz  13587  cncrng  21355  addcnlem  24821  sgmcl  27124  hvaddcl  31100  hvmulcl  31101  hicl  31168  hhssabloilem  31349  rmxynorm  43275  rmxyneg  43277  rmxy1  43279  rmxy0  43280  rmxp1  43289  rmyp1  43290  rmxm1  43291  rmym1  43292  rmxluc  43293  rmyluc  43294  rmyluc2  43295  rmxdbl  43296  rmydbl  43297  rmxypos  43304  ltrmynn0  43305  ltrmxnn0  43306  lermxnn0  43307  rmxnn  43308  ltrmy  43309  rmyeq0  43310  rmyeq  43311  lermy  43312  rmynn  43313  rmynn0  43314  rmyabs  43315  jm2.24nn  43316  jm2.17a  43317  jm2.17b  43318  jm2.17c  43319  jm2.24  43320  rmygeid  43321  jm2.18  43345  jm2.19lem1  43346  jm2.19lem2  43347  jm2.19  43350  jm2.22  43352  jm2.23  43353  jm2.20nn  43354  jm2.25  43356  jm2.26a  43357  jm2.26lem3  43358  jm2.26  43359  jm2.15nn0  43360  jm2.16nn0  43361  jm2.27a  43362  jm2.27c  43364  rmydioph  43371  rmxdiophlem  43372  jm3.1lem1  43374  jm3.1  43377  expdiophlem1  43378