Theorem fovcdm 7471

Description: An operation's value belongs to its codomain. (Contributed by NM, 27-Aug-2006.)

Assertion

Ref	Expression
fovcdm	⊢ ((𝐹:(𝑅 × 𝑆)⟶𝐶 ∧ 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝐶)

Proof of Theorem fovcdm

Step	Hyp	Ref	Expression
1		opelxpi 5634	. . 3 ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → ⟨𝐴, 𝐵⟩ ∈ (𝑅 × 𝑆))
2		df-ov 7307	. . . 4 ⊢ (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
3		ffvelcdm 6988	. . . 4 ⊢ ((𝐹:(𝑅 × 𝑆)⟶𝐶 ∧ ⟨𝐴, 𝐵⟩ ∈ (𝑅 × 𝑆)) → (𝐹‘⟨𝐴, 𝐵⟩) ∈ 𝐶)
4	2, 3	eqeltrid 2841	. . 3 ⊢ ((𝐹:(𝑅 × 𝑆)⟶𝐶 ∧ ⟨𝐴, 𝐵⟩ ∈ (𝑅 × 𝑆)) → (𝐴𝐹𝐵) ∈ 𝐶)
5	1, 4	sylan2 594	. 2 ⊢ ((𝐹:(𝑅 × 𝑆)⟶𝐶 ∧ (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆)) → (𝐴𝐹𝐵) ∈ 𝐶)
6	5	3impb 1115	1 ⊢ ((𝐹:(𝑅 × 𝑆)⟶𝐶 ∧ 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝐶)

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1087   ∈ wcel 2104  ⟨cop 4572   × cxp 5595  ⟶wf 6451  ‘cfv 6455  (class class class)co 7304

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 2707  ax-sep 5233  ax-nul 5240  ax-pr 5362

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3280  df-v 3440  df-dif 3896  df-un 3898  df-in 3900  df-ss 3910  df-nul 4264  df-if 4467  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4846  df-br 5083  df-opab 5145  df-id 5497  df-xp 5603  df-rel 5604  df-cnv 5605  df-co 5606  df-dm 5607  df-rn 5608  df-iota 6407  df-fun 6457  df-fn 6458  df-f 6459  df-fv 6463  df-ov 7307

This theorem is referenced by:  fovcdmda  7472  fovcdmd  7473  ovmpoelrn  7941  curry1f  7975  curry2f  7977  mapxpen  8965  axdc4lem  10254  axdc4uzlem  13746  imasmnd2  18464  grpsubcl  18697  imasgrp2  18732  imasring  19900  tsmsxplem1  23346  psmetcl  23502  xmetcl  23526  metcl  23527  blssm  23613  mbfi1fseqlem3  24924  mbfi1fseqlem4  24925  mbfi1fseqlem5  24926  grpocl  28904  grpodivcl  28943  vccl  28967  nvmcl  29050  cvmliftphtlem  33321  matunitlindflem1  35815  isbnd3  35984  clmgmOLD  36051  rngocl  36101  isdrngo2  36158