Theorem fovcdmd 7530

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

Syntax hints:   → wi 4   ∈ wcel 2113   × cxp 5622  ⟶wf 6488  (class class class)co 7358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500  df-ov 7361

This theorem is referenced by:  eroveu  8749  fseqenlem1  9934  rlimcn2  15514  homarel  17960  curf1cl  18151  curf2cl  18154  hofcllem  18181  yonedalem3b  18202  gasubg  19231  gacan  19234  gapm  19235  gastacos  19239  orbsta  19242  galactghm  19333  sylow1lem2  19528  sylow2alem2  19547  sylow3lem1  19556  efgcpbllemb  19684  frgpuplem  19701  frlmbas3  21731  mamucl  22345  mamuass  22346  mamudi  22347  mamudir  22348  mamuvs1  22349  mamuvs2  22350  mamulid  22385  mamurid  22386  mamutpos  22402  matgsumcl  22404  mavmulcl  22491  mavmulass  22493  mdetleib2  22532  mdetf  22539  mdetdiaglem  22542  mdetrlin  22546  mdetrsca  22547  mdetralt  22552  mdetunilem7  22562  maducoeval2  22584  madugsum  22587  madurid  22588  tsmsxplem2  24098  isxmet2d  24271  ismet2  24277  prdsxmetlem  24312  comet  24457  ipcn  25202  ovoliunlem2  25460  itg1addlem4  25656  itg1addlem5  25657  mbfi1fseqlem5  25676  limccnp2  25849  midcl  28849  conjga  33252  fedgmullem2  33787  pstmxmet  34054  cvmlift2lem9  35505  isbnd3  37981  prdsbnd  37990  iscringd  38195  rmxycomplete  43155  rmxyadd  43159  2arympt  48891