Theorem fovcdmd 7605

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

Syntax hints:   → wi 4   ∈ wcel 2108   × cxp 5683  ⟶wf 6557  (class class class)co 7431

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 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-fv 6569  df-ov 7434

This theorem is referenced by:  eroveu  8852  fseqenlem1  10064  rlimcn2  15627  homarel  18081  curf1cl  18273  curf2cl  18276  hofcllem  18303  yonedalem3b  18324  gasubg  19320  gacan  19323  gapm  19324  gastacos  19328  orbsta  19331  galactghm  19422  sylow1lem2  19617  sylow2alem2  19636  sylow3lem1  19645  efgcpbllemb  19773  frgpuplem  19790  frlmbas3  21796  mamucl  22405  mamuass  22406  mamudi  22407  mamudir  22408  mamuvs1  22409  mamuvs2  22410  mamulid  22447  mamurid  22448  mamutpos  22464  matgsumcl  22466  mavmulcl  22553  mavmulass  22555  mdetleib2  22594  mdetf  22601  mdetdiaglem  22604  mdetrlin  22608  mdetrsca  22609  mdetralt  22614  mdetunilem7  22624  maducoeval2  22646  madugsum  22649  madurid  22650  tsmsxplem2  24162  isxmet2d  24337  ismet2  24343  prdsxmetlem  24378  comet  24526  ipcn  25280  ovoliunlem2  25538  itg1addlem4  25734  itg1addlem5  25735  mbfi1fseqlem5  25754  limccnp2  25927  midcl  28785  fedgmullem2  33681  pstmxmet  33896  cvmlift2lem9  35316  isbnd3  37791  prdsbnd  37800  iscringd  38005  rmxycomplete  42929  rmxyadd  42933  2arympt  48570