Theorem fovcdmd 7572

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

Syntax hints:   → wi 4   ∈ wcel 2145   × cxp 5650  ⟶wf 6521  (class class class)co 7400

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-nul 5261  ax-pr 5395

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-opab 5168  df-id 5547  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-fv 6533  df-ov 7403

This theorem is referenced by:  eroveu  8798  fseqenlem1  9996  rlimcn2  15632  homarel  18083  curf1cl  18274  curf2cl  18277  hofcllem  18304  yonedalem3b  18325  gasubg  19363  gacan  19366  gapm  19367  gastacos  19371  orbsta  19374  galactghm  19465  sylow1lem2  19660  sylow2alem2  19679  sylow3lem1  19688  efgcpbllemb  19816  frgpuplem  19833  frlmbas3  21886  mamucl  22519  mamuass  22520  mamudi  22521  mamudir  22522  mamuvs1  22523  mamuvs2  22524  mamulid  22559  mamurid  22560  mamutpos  22576  matgsumcl  22578  mavmulcl  22665  mavmulass  22667  mdetleib2  22706  mdetf  22713  mdetdiaglem  22716  mdetrlin  22720  mdetrsca  22721  mdetralt  22726  mdetunilem7  22736  maducoeval2  22758  madugsum  22761  madurid  22762  tsmsxplem2  24272  isxmet2d  24445  ismet2  24451  prdsxmetlem  24486  comet  24631  ipcn  25366  ovoliunlem2  25623  itg1addlem4  25819  itg1addlem5  25820  mbfi1fseqlem5  25839  limccnp2  26012  midcl  29029  conjga  33403  fedgmullem2  33937  pstmxmet  34204  cvmlift2lem9  35674  isbnd3  38295  prdsbnd  38304  iscringd  38509  rmxycomplete  43506  rmxyadd  43510  2arympt  49280