Theorem fovcl 7548

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

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

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 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  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 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-fv 6546  df-ov 7423

This theorem is used by:  addclnq  11030  mulclnq  11032  adderpq  11041  mulerpq  11042  distrnq  11046  axaddcl  11236  axmulcl  11238  xaddcl  13369  xmulcl  13403  elfzoelz  13793  cncrng  21699  addcnlem  25184  sgmcl  27473  hvaddcl  31614  hvmulcl  31615  hicl  31682  hhssabloilem  31863  rmxynorm  43924  rmxyneg  43926  rmxy1  43928  rmxy0  43929  rmxp1  43938  rmyp1  43939  rmxm1  43940  rmym1  43941  rmxluc  43942  rmyluc  43943  rmyluc2  43944  rmxdbl  43945  rmydbl  43946  rmxypos  43953  ltrmynn0  43954  ltrmxnn0  43955  lermxnn0  43956  rmxnn  43957  ltrmy  43958  rmyeq0  43959  rmyeq  43960  lermy  43961  rmynn  43962  rmynn0  43963  rmyabs  43964  jm2.24nn  43965  jm2.17a  43966  jm2.17b  43967  jm2.17c  43968  jm2.24  43969  rmygeid  43970  jm2.18  43994  jm2.19lem1  43995  jm2.19lem2  43996  jm2.19  43999  jm2.22  44001  jm2.23  44002  jm2.20nn  44003  jm2.25  44005  jm2.26a  44006  jm2.26lem3  44007  jm2.26  44008  jm2.15nn0  44009  jm2.16nn0  44010  jm2.27a  44011  jm2.27c  44013  rmydioph  44020  rmxdiophlem  44021  jm3.1lem1  44023  jm3.1  44026  expdiophlem1  44027