Theorem fovrnd 7136

Description: An operation's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)

Hypotheses

Ref	Expression
fovrnd.1	⊢ (𝜑 → 𝐹:(𝑅 × 𝑆)⟶𝐶)
fovrnd.2	⊢ (𝜑 → 𝐴 ∈ 𝑅)
fovrnd.3	⊢ (𝜑 → 𝐵 ∈ 𝑆)

Assertion

Ref	Expression
fovrnd	⊢ (𝜑 → (𝐴𝐹𝐵) ∈ 𝐶)

Proof of Theorem fovrnd

Step	Hyp	Ref	Expression
1		fovrnd.1	. 2 ⊢ (𝜑 → 𝐹:(𝑅 × 𝑆)⟶𝐶)
2		fovrnd.2	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝑅)
3		fovrnd.3	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝑆)
4		fovrn 7134	. 2 ⊢ ((𝐹:(𝑅 × 𝑆)⟶𝐶 ∧ 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝐶)
5	1, 2, 3, 4	syl3anc 1351	1 ⊢ (𝜑 → (𝐴𝐹𝐵) ∈ 𝐶)

Syntax hints:   → wi 4   ∈ wcel 2050   × cxp 5405  ⟶wf 6184  (class class class)co 6976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-sep 5060  ax-nul 5067  ax-pr 5186

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ral 3093  df-rex 3094  df-rab 3097  df-v 3417  df-sbc 3682  df-dif 3832  df-un 3834  df-in 3836  df-ss 3843  df-nul 4179  df-if 4351  df-sn 4442  df-pr 4444  df-op 4448  df-uni 4713  df-br 4930  df-opab 4992  df-id 5312  df-xp 5413  df-rel 5414  df-cnv 5415  df-co 5416  df-dm 5417  df-rn 5418  df-iota 6152  df-fun 6190  df-fn 6191  df-f 6192  df-fv 6196  df-ov 6979

This theorem is referenced by:  eroveu  8192  fseqenlem1  9244  rlimcn2  14808  homarel  17154  curf1cl  17336  curf2cl  17339  hofcllem  17366  yonedalem3b  17387  gasubg  18203  gacan  18206  gapm  18207  gastacos  18211  orbsta  18214  galactghm  18292  sylow1lem2  18485  sylow2alem2  18504  sylow3lem1  18513  efgcpbllemb  18641  frgpuplem  18658  frlmbas3  20622  mamucl  20714  mamuass  20715  mamudi  20716  mamudir  20717  mamuvs1  20718  mamuvs2  20719  mamulid  20754  mamurid  20755  mamutpos  20771  matgsumcl  20773  mavmulcl  20860  mavmulass  20862  mdetleib2  20901  mdetf  20908  mdetdiaglem  20911  mdetrlin  20915  mdetrsca  20916  mdetralt  20921  mdetunilem7  20931  maducoeval2  20953  madugsum  20956  madurid  20957  tsmsxplem2  22465  isxmet2d  22640  ismet2  22646  prdsxmetlem  22681  comet  22826  ipcn  23552  ovoliunlem2  23807  itg1addlem4  24003  itg1addlem5  24004  mbfi1fseqlem5  24023  limccnp2  24193  midcl  26265  fedgmullem2  30661  pstmxmet  30787  cvmlift2lem9  32149  isbnd3  34510  prdsbnd  34519  iscringd  34724  rmxycomplete  38916  rmxyadd  38920