Theorem fovcdmd 7604

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 7602	. 2 ⊢ ((𝐹:(𝑅 × 𝑆)⟶𝐶 ∧ 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝐶)
5	1, 2, 3, 4	syl3anc 1370	1 ⊢ (𝜑 → (𝐴𝐹𝐵) ∈ 𝐶)

Syntax hints:   → wi 4   ∈ wcel 2105   × cxp 5686  ⟶wf 6558  (class class class)co 7430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-fv 6570  df-ov 7433

This theorem is referenced by:  eroveu  8850  fseqenlem1  10061  rlimcn2  15623  homarel  18089  curf1cl  18284  curf2cl  18287  hofcllem  18314  yonedalem3b  18335  gasubg  19332  gacan  19335  gapm  19336  gastacos  19340  orbsta  19343  galactghm  19436  sylow1lem2  19631  sylow2alem2  19650  sylow3lem1  19659  efgcpbllemb  19787  frgpuplem  19804  frlmbas3  21813  mamucl  22420  mamuass  22421  mamudi  22422  mamudir  22423  mamuvs1  22424  mamuvs2  22425  mamulid  22462  mamurid  22463  mamutpos  22479  matgsumcl  22481  mavmulcl  22568  mavmulass  22570  mdetleib2  22609  mdetf  22616  mdetdiaglem  22619  mdetrlin  22623  mdetrsca  22624  mdetralt  22629  mdetunilem7  22639  maducoeval2  22661  madugsum  22664  madurid  22665  tsmsxplem2  24177  isxmet2d  24352  ismet2  24358  prdsxmetlem  24393  comet  24541  ipcn  25293  ovoliunlem2  25551  itg1addlem4  25747  itg1addlem4OLD  25748  itg1addlem5  25749  mbfi1fseqlem5  25768  limccnp2  25941  midcl  28799  fedgmullem2  33657  pstmxmet  33857  cvmlift2lem9  35295  isbnd3  37770  prdsbnd  37779  iscringd  37984  rmxycomplete  42905  rmxyadd  42909  2arympt  48498