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

Theorem dffn5 6718
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 6448 . . . . 5 (𝐹 Fn 𝐴 → Rel 𝐹)
2 dfrel4v 6041 . . . . 5 (Rel 𝐹𝐹 = {⟨𝑥, 𝑦⟩ ∣ 𝑥𝐹𝑦})
31, 2sylib 219 . . . 4 (𝐹 Fn 𝐴𝐹 = {⟨𝑥, 𝑦⟩ ∣ 𝑥𝐹𝑦})
4 fnbr 6453 . . . . . . . 8 ((𝐹 Fn 𝐴𝑥𝐹𝑦) → 𝑥𝐴)
54ex 413 . . . . . . 7 (𝐹 Fn 𝐴 → (𝑥𝐹𝑦𝑥𝐴))
65pm4.71rd 563 . . . . . 6 (𝐹 Fn 𝐴 → (𝑥𝐹𝑦 ↔ (𝑥𝐴𝑥𝐹𝑦)))
7 eqcom 2828 . . . . . . . 8 (𝑦 = (𝐹𝑥) ↔ (𝐹𝑥) = 𝑦)
8 fnbrfvb 6712 . . . . . . . 8 ((𝐹 Fn 𝐴𝑥𝐴) → ((𝐹𝑥) = 𝑦𝑥𝐹𝑦))
97, 8syl5bb 284 . . . . . . 7 ((𝐹 Fn 𝐴𝑥𝐴) → (𝑦 = (𝐹𝑥) ↔ 𝑥𝐹𝑦))
109pm5.32da 579 . . . . . 6 (𝐹 Fn 𝐴 → ((𝑥𝐴𝑦 = (𝐹𝑥)) ↔ (𝑥𝐴𝑥𝐹𝑦)))
116, 10bitr4d 283 . . . . 5 (𝐹 Fn 𝐴 → (𝑥𝐹𝑦 ↔ (𝑥𝐴𝑦 = (𝐹𝑥))))
1211opabbidv 5124 . . . 4 (𝐹 Fn 𝐴 → {⟨𝑥, 𝑦⟩ ∣ 𝑥𝐹𝑦} = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = (𝐹𝑥))})
133, 12eqtrd 2856 . . 3 (𝐹 Fn 𝐴𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = (𝐹𝑥))})
14 df-mpt 5139 . . 3 (𝑥𝐴 ↦ (𝐹𝑥)) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = (𝐹𝑥))}
1513, 14syl6eqr 2874 . 2 (𝐹 Fn 𝐴𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)))
16 fvex 6677 . . . 4 (𝐹𝑥) ∈ V
17 eqid 2821 . . . 4 (𝑥𝐴 ↦ (𝐹𝑥)) = (𝑥𝐴 ↦ (𝐹𝑥))
1816, 17fnmpti 6485 . . 3 (𝑥𝐴 ↦ (𝐹𝑥)) Fn 𝐴
19 fneq1 6438 . . 3 (𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)) → (𝐹 Fn 𝐴 ↔ (𝑥𝐴 ↦ (𝐹𝑥)) Fn 𝐴))
2018, 19mpbiri 259 . 2 (𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)) → 𝐹 Fn 𝐴)
2115, 20impbii 210 1 (𝐹 Fn 𝐴𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)))
Colors of variables: wff setvar class
Syntax hints:  wb 207  wa 396   = wceq 1528  wcel 2105   class class class wbr 5058  {copab 5120  cmpt 5138  Rel wrel 5554   Fn wfn 6344  cfv 6349
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pr 5321
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-sbc 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4833  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-iota 6308  df-fun 6351  df-fn 6352  df-fv 6357
This theorem is referenced by:  fnrnfv  6719  feqmptd  6727  dffn5f  6730  eqfnfv  6795  fndmin  6808  fcompt  6888  funiun  6902  resfunexg  6970  eufnfv  6983  nvocnv  7029  fnov  7271  offveqb  7420  caofinvl  7425  oprabco  7782  df1st2  7784  df2nd2  7785  curry1  7790  curry2  7793  resixpfo  8489  pw2f1olem  8610  marypha2lem3  8890  seqof  13417  prmrec  16248  prdsbascl  16746  xpsaddlem  16836  xpsvsca  16840  oppccatid  16979  fuclid  17226  fucrid  17227  curfuncf  17478  yonedainv  17521  yonffthlem  17522  prdsidlem  17933  pws0g  17937  prdsinvlem  18148  gsummptmhm  18991  staffn  19551  prdslmodd  19672  ofco2  20990  1mavmul  21087  cnmpt1st  22206  cnmpt2nd  22207  ptunhmeo  22346  xpsxmetlem  22918  xpsmet  22921  itg2split  24279  pserulm  24939  pserdvlem2  24945  logcn  25157  logblog  25297  emcllem5  25505  gamcvg2lem  25564  crctcshlem4  27526  eucrct2eupth  27952  fcomptf  30332  gsummpt2d  30615  pl1cn  31098  esumpcvgval  31237  esumcvgsum  31247  eulerpartgbij  31530  dstfrvclim1  31635  ptpconn  32378  knoppcnlem8  33737  knoppcnlem11  33740  ctbssinf  34570  curfv  34754  ovoliunnfl  34816  voliunnfl  34818  fnopabco  34881  upixp  34887  prdsbnd  34954  prdstotbnd  34955  prdsbnd2  34956  fgraphopab  39690  expgrowthi  40545  expgrowth  40547  uzmptshftfval  40558  dvcosre  42076  fourierdlem56  42328  fourierdlem62  42334  fdmdifeqresdif  44288  offvalfv  44289
  Copyright terms: Public domain W3C validator