Theorem fovcdm 7522

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 5656	. . 3 ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → ⟨𝐴, 𝐵⟩ ∈ (𝑅 × 𝑆))
2		df-ov 7355	. . . 4 ⊢ (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
3		ffvelcdm 7020	. . . 4 ⊢ ((𝐹:(𝑅 × 𝑆)⟶𝐶 ∧ ⟨𝐴, 𝐵⟩ ∈ (𝑅 × 𝑆)) → (𝐹‘⟨𝐴, 𝐵⟩) ∈ 𝐶)
4	2, 3	eqeltrid 2835	. . 3 ⊢ ((𝐹:(𝑅 × 𝑆)⟶𝐶 ∧ ⟨𝐴, 𝐵⟩ ∈ (𝑅 × 𝑆)) → (𝐴𝐹𝐵) ∈ 𝐶)
5	1, 4	sylan2 593	. 2 ⊢ ((𝐹:(𝑅 × 𝑆)⟶𝐶 ∧ (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆)) → (𝐴𝐹𝐵) ∈ 𝐶)
6	5	3impb 1114	1 ⊢ ((𝐹:(𝑅 × 𝑆)⟶𝐶 ∧ 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   ∈ wcel 2111  ⟨cop 4581   × cxp 5617  ⟶wf 6483  ‘cfv 6487  (class class class)co 7352

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 2113  ax-9 2121  ax-10 2144  ax-12 2180  ax-ext 2703  ax-sep 5236  ax-nul 5246  ax-pr 5372

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 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-iota 6443  df-fun 6489  df-fn 6490  df-f 6491  df-fv 6495  df-ov 7355

This theorem is referenced by:  fovcdmda  7523  fovcdmd  7524  ovmpoelrn  8010  curry1f  8042  curry2f  8044  mapxpen  9062  axdc4lem  10352  axdc4uzlem  13896  imasmnd2  18688  grpsubcl  18939  imasgrp2  18974  imasring  20254  tsmsxplem1  24074  psmetcl  24228  xmetcl  24252  metcl  24253  blssm  24339  mbfi1fseqlem3  25651  mbfi1fseqlem4  25652  mbfi1fseqlem5  25653  grpocl  30487  grpodivcl  30526  vccl  30550  nvmcl  30633  cvmliftphtlem  35368  matunitlindflem1  37662  isbnd3  37830  clmgmOLD  37897  rngocl  37947  isdrngo2  38004