Theorem fovcdmd 7577

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

Syntax hints:   → wi 4   ∈ wcel 2108   × cxp 5652  ⟶wf 6526  (class class class)co 7403

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-fv 6538  df-ov 7406

This theorem is referenced by:  eroveu  8824  fseqenlem1  10036  rlimcn2  15605  homarel  18047  curf1cl  18238  curf2cl  18241  hofcllem  18268  yonedalem3b  18289  gasubg  19283  gacan  19286  gapm  19287  gastacos  19291  orbsta  19294  galactghm  19383  sylow1lem2  19578  sylow2alem2  19597  sylow3lem1  19606  efgcpbllemb  19734  frgpuplem  19751  frlmbas3  21734  mamucl  22337  mamuass  22338  mamudi  22339  mamudir  22340  mamuvs1  22341  mamuvs2  22342  mamulid  22377  mamurid  22378  mamutpos  22394  matgsumcl  22396  mavmulcl  22483  mavmulass  22485  mdetleib2  22524  mdetf  22531  mdetdiaglem  22534  mdetrlin  22538  mdetrsca  22539  mdetralt  22544  mdetunilem7  22554  maducoeval2  22576  madugsum  22579  madurid  22580  tsmsxplem2  24090  isxmet2d  24264  ismet2  24270  prdsxmetlem  24305  comet  24450  ipcn  25196  ovoliunlem2  25454  itg1addlem4  25650  itg1addlem5  25651  mbfi1fseqlem5  25670  limccnp2  25843  midcl  28702  fedgmullem2  33616  pstmxmet  33874  cvmlift2lem9  35279  isbnd3  37754  prdsbnd  37763  iscringd  37968  rmxycomplete  42888  rmxyadd  42892  2arympt  48577