ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  dffn5im GIF version

Theorem dffn5im 5363
Description: Representation of a function in terms of its values. The converse holds given the law of the excluded middle; as it is we have most of the converse via funmpt 5065 and dmmptss 4940. (Contributed by Jim Kingdon, 31-Dec-2018.)
Assertion
Ref Expression
dffn5im (𝐹 Fn 𝐴𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐹

Proof of Theorem dffn5im
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 fnrel 5125 . . . 4 (𝐹 Fn 𝐴 → Rel 𝐹)
2 dfrel4v 4895 . . . 4 (Rel 𝐹𝐹 = {⟨𝑥, 𝑦⟩ ∣ 𝑥𝐹𝑦})
31, 2sylib 121 . . 3 (𝐹 Fn 𝐴𝐹 = {⟨𝑥, 𝑦⟩ ∣ 𝑥𝐹𝑦})
4 fnbr 5129 . . . . . . 7 ((𝐹 Fn 𝐴𝑥𝐹𝑦) → 𝑥𝐴)
54ex 114 . . . . . 6 (𝐹 Fn 𝐴 → (𝑥𝐹𝑦𝑥𝐴))
65pm4.71rd 387 . . . . 5 (𝐹 Fn 𝐴 → (𝑥𝐹𝑦 ↔ (𝑥𝐴𝑥𝐹𝑦)))
7 eqcom 2091 . . . . . . 7 (𝑦 = (𝐹𝑥) ↔ (𝐹𝑥) = 𝑦)
8 fnbrfvb 5358 . . . . . . 7 ((𝐹 Fn 𝐴𝑥𝐴) → ((𝐹𝑥) = 𝑦𝑥𝐹𝑦))
97, 8syl5bb 191 . . . . . 6 ((𝐹 Fn 𝐴𝑥𝐴) → (𝑦 = (𝐹𝑥) ↔ 𝑥𝐹𝑦))
109pm5.32da 441 . . . . 5 (𝐹 Fn 𝐴 → ((𝑥𝐴𝑦 = (𝐹𝑥)) ↔ (𝑥𝐴𝑥𝐹𝑦)))
116, 10bitr4d 190 . . . 4 (𝐹 Fn 𝐴 → (𝑥𝐹𝑦 ↔ (𝑥𝐴𝑦 = (𝐹𝑥))))
1211opabbidv 3910 . . 3 (𝐹 Fn 𝐴 → {⟨𝑥, 𝑦⟩ ∣ 𝑥𝐹𝑦} = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = (𝐹𝑥))})
133, 12eqtrd 2121 . 2 (𝐹 Fn 𝐴𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = (𝐹𝑥))})
14 df-mpt 3907 . 2 (𝑥𝐴 ↦ (𝐹𝑥)) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = (𝐹𝑥))}
1513, 14syl6eqr 2139 1 (𝐹 Fn 𝐴𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103   = wceq 1290  wcel 1439   class class class wbr 3851  {copab 3904  cmpt 3905  Rel wrel 4457   Fn wfn 5023  cfv 5028
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-14 1451  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071  ax-sep 3963  ax-pow 4015  ax-pr 4045
This theorem depends on definitions:  df-bi 116  df-3an 927  df-tru 1293  df-nf 1396  df-sb 1694  df-eu 1952  df-mo 1953  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-ral 2365  df-rex 2366  df-v 2622  df-sbc 2842  df-un 3004  df-in 3006  df-ss 3013  df-pw 3435  df-sn 3456  df-pr 3457  df-op 3459  df-uni 3660  df-br 3852  df-opab 3906  df-mpt 3907  df-id 4129  df-xp 4458  df-rel 4459  df-cnv 4460  df-co 4461  df-dm 4462  df-iota 4993  df-fun 5030  df-fn 5031  df-fv 5036
This theorem is referenced by:  fnrnfv  5364  feqmptd  5370  dffn5imf  5372  eqfnfv  5411  fndmin  5420  fcompt  5481  resfunexg  5532  eufnfv  5539  fnovim  5767  offveqb  5888  caofinvl  5891  oprabco  5996  df1st2  5998  df2nd2  5999  xpen  6615
  Copyright terms: Public domain W3C validator