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

Theorem dffun7 5811
Description: Alternate definition of a function. One possibility for the definition of a function in [Enderton] p. 42. (Enderton's definition is ambiguous because "there is only one" could mean either "there is at most one" or "there is exactly one." However, dffun8 5812 shows that it doesn't matter which meaning we pick.) (Contributed by NM, 4-Nov-2002.)
Assertion
Ref Expression
dffun7 (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥 ∈ dom 𝐴∃*𝑦 𝑥𝐴𝑦))
Distinct variable group:   𝑥,𝑦,𝐴

Proof of Theorem dffun7
StepHypRef Expression
1 dffun6 5800 . 2 (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥∃*𝑦 𝑥𝐴𝑦))
2 moabs 2483 . . . . . 6 (∃*𝑦 𝑥𝐴𝑦 ↔ (∃𝑦 𝑥𝐴𝑦 → ∃*𝑦 𝑥𝐴𝑦))
3 vex 3170 . . . . . . . 8 𝑥 ∈ V
43eldm 5225 . . . . . . 7 (𝑥 ∈ dom 𝐴 ↔ ∃𝑦 𝑥𝐴𝑦)
54imbi1i 337 . . . . . 6 ((𝑥 ∈ dom 𝐴 → ∃*𝑦 𝑥𝐴𝑦) ↔ (∃𝑦 𝑥𝐴𝑦 → ∃*𝑦 𝑥𝐴𝑦))
62, 5bitr4i 265 . . . . 5 (∃*𝑦 𝑥𝐴𝑦 ↔ (𝑥 ∈ dom 𝐴 → ∃*𝑦 𝑥𝐴𝑦))
76albii 1735 . . . 4 (∀𝑥∃*𝑦 𝑥𝐴𝑦 ↔ ∀𝑥(𝑥 ∈ dom 𝐴 → ∃*𝑦 𝑥𝐴𝑦))
8 df-ral 2895 . . . 4 (∀𝑥 ∈ dom 𝐴∃*𝑦 𝑥𝐴𝑦 ↔ ∀𝑥(𝑥 ∈ dom 𝐴 → ∃*𝑦 𝑥𝐴𝑦))
97, 8bitr4i 265 . . 3 (∀𝑥∃*𝑦 𝑥𝐴𝑦 ↔ ∀𝑥 ∈ dom 𝐴∃*𝑦 𝑥𝐴𝑦)
109anbi2i 725 . 2 ((Rel 𝐴 ∧ ∀𝑥∃*𝑦 𝑥𝐴𝑦) ↔ (Rel 𝐴 ∧ ∀𝑥 ∈ dom 𝐴∃*𝑦 𝑥𝐴𝑦))
111, 10bitri 262 1 (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥 ∈ dom 𝐴∃*𝑦 𝑥𝐴𝑦))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382  wal 1472  wex 1694  wcel 1975  ∃*wmo 2453  wral 2890   class class class wbr 4572  dom cdm 5023  Rel wrel 5028  Fun wfun 5779
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2227  ax-ext 2584  ax-sep 4698  ax-nul 4707  ax-pr 4823
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2456  df-mo 2457  df-clab 2591  df-cleq 2597  df-clel 2600  df-nfc 2734  df-ral 2895  df-rab 2899  df-v 3169  df-dif 3537  df-un 3539  df-in 3541  df-ss 3548  df-nul 3869  df-if 4031  df-sn 4120  df-pr 4122  df-op 4126  df-br 4573  df-opab 4633  df-id 4938  df-cnv 5031  df-co 5032  df-dm 5033  df-fun 5787
This theorem is referenced by:  dffun8  5812  dffun9  5813  brdom5  9204  imasaddfnlem  15952  imasvscafn  15961  funressnfv  39656
  Copyright terms: Public domain W3C validator