Theorem dffun6 6551

Description: Alternate definition of a function using "at most one" notation. (Contributed by NM, 9-Mar-1995.) Avoid ax-10 2179, ax-12 2216. (Revised by SN, 19-Dec-2024.)

Assertion

Ref	Expression
dffun6	⊢ (Fun 𝐹 ↔ (Rel 𝐹 ∧ ∀𝑥∃*𝑦 𝑥𝐹𝑦))

Distinct variable group:   𝑥,𝐹,𝑦

Proof of Theorem dffun6

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dffun2 6550	. 2 ⊢ (Fun 𝐹 ↔ (Rel 𝐹 ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝐹𝑦 ∧ 𝑥𝐹𝑧) → 𝑦 = 𝑧)))
2		breq2 5115	. . . . 5 ⊢ (𝑦 = 𝑧 → (𝑥𝐹𝑦 ↔ 𝑥𝐹𝑧))
3	2	mo4 2596	. . . 4 ⊢ (∃*𝑦 𝑥𝐹𝑦 ↔ ∀𝑦∀𝑧((𝑥𝐹𝑦 ∧ 𝑥𝐹𝑧) → 𝑦 = 𝑧))
4	3	albii 1852	. . 3 ⊢ (∀𝑥∃*𝑦 𝑥𝐹𝑦 ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝐹𝑦 ∧ 𝑥𝐹𝑧) → 𝑦 = 𝑧))
5	4	anbi2i 635	. 2 ⊢ ((Rel 𝐹 ∧ ∀𝑥∃*𝑦 𝑥𝐹𝑦) ↔ (Rel 𝐹 ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝐹𝑦 ∧ 𝑥𝐹𝑧) → 𝑦 = 𝑧)))
6	1, 5	bitr4i 281	1 ⊢ (Fun 𝐹 ↔ (Rel 𝐹 ∧ ∀𝑥∃*𝑦 𝑥𝐹𝑦))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568  ∃*wmo 2567   class class class wbr 5111  Rel wrel 5668  Fun wfun 6534

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-mo 2569  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-opab 5176  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-fun 6542

This theorem is used by:  dffun3  6552  funmo  6556  dffun7  6567  fununfun  6588  funcnvsn  6590  funcnv2  6608  svrelfun  6612  funimaexg  6626  fnres  6666  nfunsn  6924  dff3  7099  brdom3  10527  nqerf  10930  shftfn  15134  cnextfun  24272  perfdvf  26113  taylf  26575  funressnvmo  47840