Theorem euf 1011

Description: A version of the existential uniqueness definition with a hypothesis instead of a distinct variable condition.

Hypothesis

Ref	Expression
euf.1	⊢ (φ → ∀yφ)

Assertion

Ref	Expression
euf	⊢ (∃!xφ ↔ ∃y∀x(φ ↔ x = y))

Distinct variable group(s):   x,y

Proof of Theorem euf

Step	Hyp	Ref	Expression
1		df-eu 1009	. 2 ⊢ (∃!xφ ↔ ∃z∀x(φ ↔ x = z))
2		euf.1	. . . . 5 ⊢ (φ → ∀yφ)
3		ax-17 925	. . . . 5 ⊢ (x = z → ∀y x = z)
4	2, 3	hbbi 705	. . . 4 ⊢ ((φ ↔ x = z) → ∀y(φ ↔ x = z))
5	4	hbal 700	. . 3 ⊢ (∀x(φ ↔ x = z) → ∀y∀x(φ ↔ x = z))
6		ax-17 925	. . 3 ⊢ (∀x(φ ↔ x = y) → ∀z∀x(φ ↔ x = y))
7		eqt2b 818	. . . . 5 ⊢ (z = y → (x = z ↔ x = y))
8	7	bibi2d 470	. . . 4 ⊢ (z = y → ((φ ↔ x = z) ↔ (φ ↔ x = y)))
9	8	bialdv 935	. . 3 ⊢ (z = y → (∀x(φ ↔ x = z) ↔ ∀x(φ ↔ x = y)))
10	5, 6, 9	cbvex 849	. 2 ⊢ (∃z∀x(φ ↔ x = z) ↔ ∃y∀x(φ ↔ x = y))
11	1, 10	bitr 151	1 ⊢ (∃!xφ ↔ ∃y∀x(φ ↔ x = y))

Syntax hints:   → wi 2   ↔ wb 127  ∀wal 672  ∃wex 678   = weq 797  ∃!weu 1007

This theorem is referenced by:  eu1 1019  eumo0 1022

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-12.nbsp;802  ax-17 925

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-eu 1009

metamath.org