Theorem fovcdmd 7617

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147   × cxp 5653  ⟶wf 6554  (class class class)co 7443

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-fv 6566  df-ov 7446

This theorem is used by:  eroveu  8861  fseqenlem1  10130  rlimcn2  15787  homarel  18240  curf1cl  18431  curf2cl  18434  hofcllem  18461  yonedalem3b  18482  gasubg  19546  gacan  19549  gapm  19550  gastacos  19554  orbsta  19557  galactghm  19648  sylow1lem2  19843  sylow2alem2  19862  sylow3lem1  19871  efgcpbllemb  19999  frgpuplem  20016  frlmbas3  22112  mamucl  22746  mamuass  22747  mamudi  22748  mamudir  22749  mamuvs1  22750  mamuvs2  22751  mamulid  22786  mamurid  22787  mamutpos  22803  matgsumcl  22805  mavmulcl  22892  mavmulass  22894  mdetleib2  22933  mdetf  22940  mdetdiaglem  22943  mdetrlin  22947  mdetrsca  22948  mdetralt  22953  mdetunilem7  22963  maducoeval2  22985  madugsum  22988  madurid  22989  tsmsxplem2  24503  isxmet2d  24676  ismet2  24682  prdsxmetlem  24717  comet  24862  ipcn  25597  ovoliunlem2  25854  itg1addlem4  26050  itg1addlem5  26051  mbfi1fseqlem5  26070  limccnp2  26242  midcl  29312  conjga  33801  fedgmullem2  34332  pstmxmet  34599  cvmlift2lem9  36243  isbnd3  38910  prdsbnd  38919  iscringd  39124  rmxycomplete  44117  rmxyadd  44121  2arympt  49966