Theorem fovcl 7579

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2147   × cxp 5656  ⟶wf 6562  (class class class)co 7451

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-iun 4958  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-fv 6574  df-ov 7454

This theorem is used by:  addclnq  11069  mulclnq  11071  adderpq  11080  mulerpq  11081  distrnq  11085  axaddcl  11275  axmulcl  11277  xaddcl  13409  xmulcl  13443  elfzoelz  13833  cncrng  21751  addcnlem  25239  sgmcl  27530  hvaddcl  31671  hvmulcl  31672  hicl  31739  hhssabloilem  31920  j00smo  36046  rmxynorm  44191  rmxyneg  44193  rmxy1  44195  rmxy0  44196  rmxp1  44205  rmyp1  44206  rmxm1  44207  rmym1  44208  rmxluc  44209  rmyluc  44210  rmyluc2  44211  rmxdbl  44212  rmydbl  44213  rmxypos  44220  ltrmynn0  44221  ltrmxnn0  44222  lermxnn0  44223  rmxnn  44224  ltrmy  44225  rmyeq0  44226  rmyeq  44227  lermy  44228  rmynn  44229  rmynn0  44230  rmyabs  44231  jm2.24nn  44232  jm2.17a  44233  jm2.17b  44234  jm2.17c  44235  jm2.24  44236  rmygeid  44237  jm2.18  44261  jm2.19lem1  44262  jm2.19lem2  44263  jm2.19  44266  jm2.22  44268  jm2.23  44269  jm2.20nn  44270  jm2.25  44272  jm2.26a  44273  jm2.26lem3  44274  jm2.26  44275  jm2.15nn0  44276  jm2.16nn0  44277  jm2.27a  44278  jm2.27c  44280  rmydioph  44287  rmxdiophlem  44288  jm3.1lem1  44290  jm3.1  44293  expdiophlem1  44294