Theorem fovcdmd 7532

Description: An operation's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)

Hypotheses

Ref	Expression
fovcdmd.1	⊢ (𝜑 → 𝐹:(𝑅 × 𝑆)⟶𝐶)
fovcdmd.2	⊢ (𝜑 → 𝐴 ∈ 𝑅)
fovcdmd.3	⊢ (𝜑 → 𝐵 ∈ 𝑆)

Assertion

Ref	Expression
fovcdmd	⊢ (𝜑 → (𝐴𝐹𝐵) ∈ 𝐶)

Proof of Theorem fovcdmd

Step	Hyp	Ref	Expression
1		fovcdmd.1	. 2 ⊢ (𝜑 → 𝐹:(𝑅 × 𝑆)⟶𝐶)
2		fovcdmd.2	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝑅)
3		fovcdmd.3	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝑆)
4		fovcdm 7530	. 2 ⊢ ((𝐹:(𝑅 × 𝑆)⟶𝐶 ∧ 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝐶)
5	1, 2, 3, 4	syl3anc 1374	1 ⊢ (𝜑 → (𝐴𝐹𝐵) ∈ 𝐶)

Syntax hints:   → wi 4   ∈ wcel 2114   × cxp 5622  ⟶wf 6488  (class class class)co 7360

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500  df-ov 7363

This theorem is referenced by:  eroveu  8752  fseqenlem1  9937  rlimcn2  15544  homarel  17994  curf1cl  18185  curf2cl  18188  hofcllem  18215  yonedalem3b  18236  gasubg  19268  gacan  19271  gapm  19272  gastacos  19276  orbsta  19279  galactghm  19370  sylow1lem2  19565  sylow2alem2  19584  sylow3lem1  19593  efgcpbllemb  19721  frgpuplem  19738  frlmbas3  21766  mamucl  22376  mamuass  22377  mamudi  22378  mamudir  22379  mamuvs1  22380  mamuvs2  22381  mamulid  22416  mamurid  22417  mamutpos  22433  matgsumcl  22435  mavmulcl  22522  mavmulass  22524  mdetleib2  22563  mdetf  22570  mdetdiaglem  22573  mdetrlin  22577  mdetrsca  22578  mdetralt  22583  mdetunilem7  22593  maducoeval2  22615  madugsum  22618  madurid  22619  tsmsxplem2  24129  isxmet2d  24302  ismet2  24308  prdsxmetlem  24343  comet  24488  ipcn  25223  ovoliunlem2  25480  itg1addlem4  25676  itg1addlem5  25677  mbfi1fseqlem5  25696  limccnp2  25869  midcl  28859  conjga  33246  fedgmullem2  33790  pstmxmet  34057  cvmlift2lem9  35509  isbnd3  38119  prdsbnd  38128  iscringd  38333  rmxycomplete  43363  rmxyadd  43367  2arympt  49137