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

Theorem dffn5 6228
Description: Representation of a function in terms of its values. (Contributed by FL, 14-Sep-2013.) (Proof shortened by Mario Carneiro, 31-Aug-2015.)
Assertion
Ref Expression
dffn5 (𝐹 Fn 𝐴𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐹

Proof of Theorem dffn5
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 fnrel 5977 . . . . 5 (𝐹 Fn 𝐴 → Rel 𝐹)
2 dfrel4v 5572 . . . . 5 (Rel 𝐹𝐹 = {⟨𝑥, 𝑦⟩ ∣ 𝑥𝐹𝑦})
31, 2sylib 208 . . . 4 (𝐹 Fn 𝐴𝐹 = {⟨𝑥, 𝑦⟩ ∣ 𝑥𝐹𝑦})
4 fnbr 5981 . . . . . . . 8 ((𝐹 Fn 𝐴𝑥𝐹𝑦) → 𝑥𝐴)
54ex 450 . . . . . . 7 (𝐹 Fn 𝐴 → (𝑥𝐹𝑦𝑥𝐴))
65pm4.71rd 666 . . . . . 6 (𝐹 Fn 𝐴 → (𝑥𝐹𝑦 ↔ (𝑥𝐴𝑥𝐹𝑦)))
7 eqcom 2627 . . . . . . . 8 (𝑦 = (𝐹𝑥) ↔ (𝐹𝑥) = 𝑦)
8 fnbrfvb 6223 . . . . . . . 8 ((𝐹 Fn 𝐴𝑥𝐴) → ((𝐹𝑥) = 𝑦𝑥𝐹𝑦))
97, 8syl5bb 272 . . . . . . 7 ((𝐹 Fn 𝐴𝑥𝐴) → (𝑦 = (𝐹𝑥) ↔ 𝑥𝐹𝑦))
109pm5.32da 672 . . . . . 6 (𝐹 Fn 𝐴 → ((𝑥𝐴𝑦 = (𝐹𝑥)) ↔ (𝑥𝐴𝑥𝐹𝑦)))
116, 10bitr4d 271 . . . . 5 (𝐹 Fn 𝐴 → (𝑥𝐹𝑦 ↔ (𝑥𝐴𝑦 = (𝐹𝑥))))
1211opabbidv 4707 . . . 4 (𝐹 Fn 𝐴 → {⟨𝑥, 𝑦⟩ ∣ 𝑥𝐹𝑦} = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = (𝐹𝑥))})
133, 12eqtrd 2654 . . 3 (𝐹 Fn 𝐴𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = (𝐹𝑥))})
14 df-mpt 4721 . . 3 (𝑥𝐴 ↦ (𝐹𝑥)) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = (𝐹𝑥))}
1513, 14syl6eqr 2672 . 2 (𝐹 Fn 𝐴𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)))
16 fvex 6188 . . . 4 (𝐹𝑥) ∈ V
17 eqid 2620 . . . 4 (𝑥𝐴 ↦ (𝐹𝑥)) = (𝑥𝐴 ↦ (𝐹𝑥))
1816, 17fnmpti 6009 . . 3 (𝑥𝐴 ↦ (𝐹𝑥)) Fn 𝐴
19 fneq1 5967 . . 3 (𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)) → (𝐹 Fn 𝐴 ↔ (𝑥𝐴 ↦ (𝐹𝑥)) Fn 𝐴))
2018, 19mpbiri 248 . 2 (𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)) → 𝐹 Fn 𝐴)
2115, 20impbii 199 1 (𝐹 Fn 𝐴𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 384   = wceq 1481  wcel 1988   class class class wbr 4644  {copab 4703  cmpt 4720  Rel wrel 5109   Fn wfn 5871  cfv 5876
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pr 4897
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-sbc 3430  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-opab 4704  df-mpt 4721  df-id 5014  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-iota 5839  df-fun 5878  df-fn 5879  df-fv 5884
This theorem is referenced by:  fnrnfv  6229  feqmptd  6236  dffn5f  6239  eqfnfv  6297  fndmin  6310  fcompt  6385  funiun  6397  resfunexg  6464  eufnfv  6476  nvocnv  6522  fnov  6753  offveqb  6904  caofinvl  6909  oprabco  7246  df1st2  7248  df2nd2  7249  curry1  7254  curry2  7257  resixpfo  7931  pw2f1olem  8049  marypha2lem3  8328  seqof  12841  prmrec  15607  prdsbascl  16124  xpsaddlem  16216  xpsvsca  16220  oppccatid  16360  fuclid  16607  fucrid  16608  curfuncf  16859  yonedainv  16902  yonffthlem  16903  prdsidlem  17303  pws0g  17307  prdsinvlem  17505  gsummptmhm  18321  staffn  18830  prdslmodd  18950  ofco2  20238  1mavmul  20335  cnmpt1st  21452  cnmpt2nd  21453  ptunhmeo  21592  xpsxmetlem  22165  xpsmet  22168  itg2split  23497  pserulm  24157  pserdvlem2  24163  logcn  24374  logblog  24511  emcllem5  24707  gamcvg2lem  24766  crctcshlem4  26693  eucrct2eupth  27085  fcomptf  29431  gsummpt2d  29755  pl1cn  29975  esumpcvgval  30114  esumcvgsum  30124  eulerpartgbij  30408  dstfrvclim1  30513  ptpconn  31189  knoppcnlem8  32465  knoppcnlem11  32468  curfv  33360  ovoliunnfl  33422  voliunnfl  33424  fnopabco  33488  upixp  33495  prdsbnd  33563  prdstotbnd  33564  prdsbnd2  33565  fgraphopab  37607  expgrowthi  38352  expgrowth  38354  uzmptshftfval  38365  dvcosre  39889  fourierdlem56  40142  fourierdlem62  40148  fdmdifeqresdif  41885  offvalfv  41886
  Copyright terms: Public domain W3C validator