text: # Metamath Proof Explorer
  
  ## Theorem dffun3
  
  Description: Alternate definition of function. (Contributed by NM, 29-Dec-1996)
  
  Ref Expression
  Assertion dffun3 ${⊢}\mathrm{Fun}{A}↔\left(\mathrm{Rel}{A}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{A}{y}\to {y}={z}\right)\right)$
  
  ### Proof
  
  Step Hyp Ref Expression
  1 dffun2 ${⊢}\mathrm{Fun}{A}↔\left(\mathrm{Rel}{A}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({x}{A}{y}\wedge {x}{A}{z}\right)\to {y}={z}\right)\right)$
  2 breq2 ${⊢}{y}={z}\to \left({x}{A}{y}↔{x}{A}{z}\right)$
  3 2 mo4 ${⊢}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{x}{A}{y}↔\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({x}{A}{y}\wedge {x}{A}{z}\right)\to {y}={z}\right)$
  4 df-mo ${⊢}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{x}{A}{y}↔\exists {z}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{A}{y}\to {y}={z}\right)$
  5 3 4 bitr3i ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({x}{A}{y}\wedge {x}{A}{z}\right)\to {y}={z}\right)↔\exists {z}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{A}{y}\to {y}={z}\right)$
  6 5 albii ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({x}{A}{y}\wedge {x}{A}{z}\right)\to {y}={z}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{A}{y}\to {y}={z}\right)$
  7 6 anbi2i ${⊢}\left(\mathrm{Rel}{A}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({x}{A}{y}\wedge {x}{A}{z}\right)\to {y}={z}\right)\right)↔\left(\mathrm{Rel}{A}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{A}{y}\to {y}={z}\right)\right)$
  8 1 7 bitri ${⊢}\mathrm{Fun}{A}↔\left(\mathrm{Rel}{A}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{A}{y}\to {y}={z}\right)\right)$
metadata: {"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 9, "mathjax_tag": 0, "mathjax_inline_tex": 0, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0}