Theorem fovcdmd 7595

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   × cxp 5664  ⟶wf 6539  (class class class)co 7423

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pr 5409

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 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-ne 2962  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551  df-ov 7426

This theorem is used by:  eroveu  8819  fseqenlem1  10027  rlimcn2  15668  homarel  18118  curf1cl  18309  curf2cl  18312  hofcllem  18339  yonedalem3b  18360  gasubg  19403  gacan  19406  gapm  19407  gastacos  19411  orbsta  19414  galactghm  19505  sylow1lem2  19700  sylow2alem2  19719  sylow3lem1  19728  efgcpbllemb  19856  frgpuplem  19873  frlmbas3  21963  mamucl  22595  mamuass  22596  mamudi  22597  mamudir  22598  mamuvs1  22599  mamuvs2  22600  mamulid  22635  mamurid  22636  mamutpos  22652  matgsumcl  22654  mavmulcl  22741  mavmulass  22743  mdetleib2  22782  mdetf  22789  mdetdiaglem  22792  mdetrlin  22796  mdetrsca  22797  mdetralt  22802  mdetunilem7  22812  maducoeval2  22834  madugsum  22837  madurid  22838  tsmsxplem2  24348  isxmet2d  24521  ismet2  24527  prdsxmetlem  24562  comet  24707  ipcn  25442  ovoliunlem2  25699  itg1addlem4  25895  itg1addlem5  25896  mbfi1fseqlem5  25915  limccnp2  26088  midcl  29123  conjga  33521  fedgmullem2  34051  pstmxmet  34318  cvmlift2lem9  35823  isbnd3  38475  prdsbnd  38484  iscringd  38689  rmxycomplete  43684  rmxyadd  43688  2arympt  49469