Theorem fovcdmd 7581

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

Syntax hints:   → wi 4   ∈ wcel 2104   × cxp 5673  ⟶wf 6538  (class class class)co 7411

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-fv 6550  df-ov 7414

This theorem is referenced by:  eroveu  8808  fseqenlem1  10021  rlimcn2  15539  homarel  17990  curf1cl  18185  curf2cl  18188  hofcllem  18215  yonedalem3b  18236  gasubg  19207  gacan  19210  gapm  19211  gastacos  19215  orbsta  19218  galactghm  19313  sylow1lem2  19508  sylow2alem2  19527  sylow3lem1  19536  efgcpbllemb  19664  frgpuplem  19681  frlmbas3  21550  mamucl  22121  mamuass  22122  mamudi  22123  mamudir  22124  mamuvs1  22125  mamuvs2  22126  mamulid  22163  mamurid  22164  mamutpos  22180  matgsumcl  22182  mavmulcl  22269  mavmulass  22271  mdetleib2  22310  mdetf  22317  mdetdiaglem  22320  mdetrlin  22324  mdetrsca  22325  mdetralt  22330  mdetunilem7  22340  maducoeval2  22362  madugsum  22365  madurid  22366  tsmsxplem2  23878  isxmet2d  24053  ismet2  24059  prdsxmetlem  24094  comet  24242  ipcn  24994  ovoliunlem2  25252  itg1addlem4  25448  itg1addlem4OLD  25449  itg1addlem5  25450  mbfi1fseqlem5  25469  limccnp2  25641  midcl  28295  fedgmullem2  33003  pstmxmet  33175  cvmlift2lem9  34600  isbnd3  36955  prdsbnd  36964  iscringd  37169  rmxycomplete  41958  rmxyadd  41962  2arympt  47422