MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fovrnda Structured version   Visualization version   GIF version

Theorem fovrnda 7002
Description: An operation's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)
Hypothesis
Ref Expression
fovrnd.1 (𝜑𝐹:(𝑅 × 𝑆)⟶𝐶)
Assertion
Ref Expression
fovrnda ((𝜑 ∧ (𝐴𝑅𝐵𝑆)) → (𝐴𝐹𝐵) ∈ 𝐶)

Proof of Theorem fovrnda
StepHypRef Expression
1 fovrnd.1 . . 3 (𝜑𝐹:(𝑅 × 𝑆)⟶𝐶)
2 fovrn 7001 . . 3 ((𝐹:(𝑅 × 𝑆)⟶𝐶𝐴𝑅𝐵𝑆) → (𝐴𝐹𝐵) ∈ 𝐶)
31, 2syl3an1 1202 . 2 ((𝜑𝐴𝑅𝐵𝑆) → (𝐴𝐹𝐵) ∈ 𝐶)
433expb 1149 1 ((𝜑 ∧ (𝐴𝑅𝐵𝑆)) → (𝐴𝐹𝐵) ∈ 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wcel 2155   × cxp 5274  wf 6063  (class class class)co 6841
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742  ax-sep 4940  ax-nul 4948  ax-pr 5061
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2564  df-eu 2581  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ral 3059  df-rex 3060  df-rab 3063  df-v 3351  df-sbc 3596  df-dif 3734  df-un 3736  df-in 3738  df-ss 3745  df-nul 4079  df-if 4243  df-sn 4334  df-pr 4336  df-op 4340  df-uni 4594  df-br 4809  df-opab 4871  df-id 5184  df-xp 5282  df-rel 5283  df-cnv 5284  df-co 5285  df-dm 5286  df-rn 5287  df-iota 6030  df-fun 6069  df-fn 6070  df-f 6071  df-fv 6075  df-ov 6844
This theorem is referenced by:  eroprf  8048  yonedalem3  17187  yonedainv  17188  gass  17998  mamulid  20522  mamurid  20523  maducoeval2  20722  madutpos  20724  madugsum  20725  madurid  20726  isxmet2d  22410  prdsxmetlem  22451  rrxds  23469  ofrn  29825  metideq  30317  sibfof  30783
  Copyright terms: Public domain W3C validator