Theorem fovcl 7280

Description: Closure law for an operation. (Contributed by NM, 19-Apr-2007.)

Hypothesis

Ref	Expression
fovcl.1	⊢ 𝐹:(𝑅 × 𝑆)⟶𝐶

Assertion

Ref	Expression
fovcl	⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝐶)

Proof of Theorem fovcl

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fovcl.1	. . 3 ⊢ 𝐹:(𝑅 × 𝑆)⟶𝐶
2		ffnov 7279	. . . 4 ⊢ (𝐹:(𝑅 × 𝑆)⟶𝐶 ↔ (𝐹 Fn (𝑅 × 𝑆) ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 (𝑥𝐹𝑦) ∈ 𝐶))
3	2	simprbi 500	. . 3 ⊢ (𝐹:(𝑅 × 𝑆)⟶𝐶 → ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 (𝑥𝐹𝑦) ∈ 𝐶)
4	1, 3	ax-mp 5	. 2 ⊢ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 (𝑥𝐹𝑦) ∈ 𝐶
5		oveq1 7163	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥𝐹𝑦) = (𝐴𝐹𝑦))
6	5	eleq1d 2836	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥𝐹𝑦) ∈ 𝐶 ↔ (𝐴𝐹𝑦) ∈ 𝐶))
7		oveq2 7164	. . . 4 ⊢ (𝑦 = 𝐵 → (𝐴𝐹𝑦) = (𝐴𝐹𝐵))
8	7	eleq1d 2836	. . 3 ⊢ (𝑦 = 𝐵 → ((𝐴𝐹𝑦) ∈ 𝐶 ↔ (𝐴𝐹𝐵) ∈ 𝐶))
9	6, 8	rspc2v 3553	. 2 ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 (𝑥𝐹𝑦) ∈ 𝐶 → (𝐴𝐹𝐵) ∈ 𝐶))
10	4, 9	mpi 20	1 ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝐶)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∀wral 3070   × cxp 5526   Fn wfn 6335  ⟶wf 6336  (class class class)co 7156

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5173  ax-nul 5180  ax-pr 5302

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ral 3075  df-rex 3076  df-v 3411  df-sbc 3699  df-csb 3808  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-nul 4228  df-if 4424  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-iun 4888  df-br 5037  df-opab 5099  df-mpt 5117  df-id 5434  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-iota 6299  df-fun 6342  df-fn 6343  df-f 6344  df-fv 6348  df-ov 7159

This theorem is referenced by:  addclnq  10418  mulclnq  10420  adderpq  10429  mulerpq  10430  distrnq  10434  axaddcl  10624  axmulcl  10626  xaddcl  12686  xmulcl  12720  elfzoelz  13100  addcnlem  23579  sgmcl  25844  hvaddcl  28908  hvmulcl  28909  hicl  28976  hhssabloilem  29157  rmxynorm  40277  rmxyneg  40279  rmxy1  40281  rmxy0  40282  rmxp1  40291  rmyp1  40292  rmxm1  40293  rmym1  40294  rmxluc  40295  rmyluc  40296  rmyluc2  40297  rmxdbl  40298  rmydbl  40299  rmxypos  40306  ltrmynn0  40307  ltrmxnn0  40308  lermxnn0  40309  rmxnn  40310  ltrmy  40311  rmyeq0  40312  rmyeq  40313  lermy  40314  rmynn  40315  rmynn0  40316  rmyabs  40317  jm2.24nn  40318  jm2.17a  40319  jm2.17b  40320  jm2.17c  40321  jm2.24  40322  rmygeid  40323  jm2.18  40347  jm2.19lem1  40348  jm2.19lem2  40349  jm2.19  40352  jm2.22  40354  jm2.23  40355  jm2.20nn  40356  jm2.25  40358  jm2.26a  40359  jm2.26lem3  40360  jm2.26  40361  jm2.15nn0  40362  jm2.16nn0  40363  jm2.27a  40364  jm2.27c  40366  rmydioph  40373  rmxdiophlem  40374  jm3.1lem1  40376  jm3.1  40379  expdiophlem1  40380