Theorem fovcdmd 7535

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

Syntax hints:   → wi 4   ∈ wcel 2119   × cxp 5623  ⟶wf 6488  (class class class)co 7363

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500  df-ov 7366

This theorem is referenced by:  eroveu  8756  fseqenlem1  9944  rlimcn2  15551  homarel  18001  curf1cl  18192  curf2cl  18195  hofcllem  18222  yonedalem3b  18243  gasubg  19275  gacan  19278  gapm  19279  gastacos  19283  orbsta  19286  galactghm  19377  sylow1lem2  19572  sylow2alem2  19591  sylow3lem1  19600  efgcpbllemb  19728  frgpuplem  19745  frlmbas3  21758  mamucl  22391  mamuass  22392  mamudi  22393  mamudir  22394  mamuvs1  22395  mamuvs2  22396  mamulid  22431  mamurid  22432  mamutpos  22448  matgsumcl  22450  mavmulcl  22537  mavmulass  22539  mdetleib2  22578  mdetf  22585  mdetdiaglem  22588  mdetrlin  22592  mdetrsca  22593  mdetralt  22598  mdetunilem7  22608  maducoeval2  22630  madugsum  22633  madurid  22634  tsmsxplem2  24144  isxmet2d  24317  ismet2  24323  prdsxmetlem  24358  comet  24503  ipcn  25238  ovoliunlem2  25495  itg1addlem4  25691  itg1addlem5  25692  mbfi1fseqlem5  25711  limccnp2  25884  midcl  28870  conjga  33258  fedgmullem2  33821  pstmxmet  34088  cvmlift2lem9  35546  isbnd3  38158  prdsbnd  38167  iscringd  38372  rmxycomplete  43369  rmxyadd  43373  2arympt  49147