Theorem fovcl 7542

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145   × cxp 5653  ⟶wf 6529  (class class class)co 7414

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-fv 6541  df-ov 7417

This theorem is used by:  addclnq  10955  mulclnq  10957  adderpq  10966  mulerpq  10967  distrnq  10971  axaddcl  11161  axmulcl  11163  xaddcl  13292  xmulcl  13326  elfzoelz  13715  cncrng  21607  addcnlem  25092  sgmcl  27383  hvaddcl  31494  hvmulcl  31495  hicl  31562  hhssabloilem  31743  rmxynorm  43760  rmxyneg  43762  rmxy1  43764  rmxy0  43765  rmxp1  43774  rmyp1  43775  rmxm1  43776  rmym1  43777  rmxluc  43778  rmyluc  43779  rmyluc2  43780  rmxdbl  43781  rmydbl  43782  rmxypos  43789  ltrmynn0  43790  ltrmxnn0  43791  lermxnn0  43792  rmxnn  43793  ltrmy  43794  rmyeq0  43795  rmyeq  43796  lermy  43797  rmynn  43798  rmynn0  43799  rmyabs  43800  jm2.24nn  43801  jm2.17a  43802  jm2.17b  43803  jm2.17c  43804  jm2.24  43805  rmygeid  43806  jm2.18  43830  jm2.19lem1  43831  jm2.19lem2  43832  jm2.19  43835  jm2.22  43837  jm2.23  43838  jm2.20nn  43839  jm2.25  43841  jm2.26a  43842  jm2.26lem3  43843  jm2.26  43844  jm2.15nn0  43845  jm2.16nn0  43846  jm2.27a  43847  jm2.27c  43849  rmydioph  43856  rmxdiophlem  43857  jm3.1lem1  43859  jm3.1  43862  expdiophlem1  43863