Theorem fovcl 7517

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   × cxp 5636  ⟶wf 6507  (class class class)co 7387

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-fv 6519  df-ov 7390

This theorem is referenced by:  addclnq  10898  mulclnq  10900  adderpq  10909  mulerpq  10910  distrnq  10914  axaddcl  11104  axmulcl  11106  xaddcl  13199  xmulcl  13233  elfzoelz  13620  cncrng  21300  addcnlem  24753  sgmcl  27056  hvaddcl  30941  hvmulcl  30942  hicl  31009  hhssabloilem  31190  rmxynorm  42907  rmxyneg  42909  rmxy1  42911  rmxy0  42912  rmxp1  42921  rmyp1  42922  rmxm1  42923  rmym1  42924  rmxluc  42925  rmyluc  42926  rmyluc2  42927  rmxdbl  42928  rmydbl  42929  rmxypos  42936  ltrmynn0  42937  ltrmxnn0  42938  lermxnn0  42939  rmxnn  42940  ltrmy  42941  rmyeq0  42942  rmyeq  42943  lermy  42944  rmynn  42945  rmynn0  42946  rmyabs  42947  jm2.24nn  42948  jm2.17a  42949  jm2.17b  42950  jm2.17c  42951  jm2.24  42952  rmygeid  42953  jm2.18  42977  jm2.19lem1  42978  jm2.19lem2  42979  jm2.19  42982  jm2.22  42984  jm2.23  42985  jm2.20nn  42986  jm2.25  42988  jm2.26a  42989  jm2.26lem3  42990  jm2.26  42991  jm2.15nn0  42992  jm2.16nn0  42993  jm2.27a  42994  jm2.27c  42996  rmydioph  43003  rmxdiophlem  43004  jm3.1lem1  43006  jm3.1  43009  expdiophlem1  43010