Theorem bieu 1014

Description: Introduce uniqueness quantifier to both sides of an equivalence.

Hypothesis

Ref	Expression
bieu.1	⊢ (φ ↔ ψ)

Assertion

Ref	Expression
bieu	⊢ (∃!xφ ↔ ∃!xψ)

Proof of Theorem bieu

Step	Hyp	Ref	Expression
1		eqid 810	. 2 ⊢ x = x
2	1	hbth 697	. . 3 ⊢ (x = x → ∀x x = x)
3		bieu.1	. . . 4 ⊢ (φ ↔ ψ)
4	3	a1i 7	. . 3 ⊢ (x = x → (φ ↔ ψ))
5	2, 4	bieud 1012	. 2 ⊢ (x = x → (∃!xφ ↔ ∃!xψ))
6	1, 5	ax-mp 6	1 ⊢ (∃!xφ ↔ ∃!xψ)

Syntax hints:   ↔ wb 127   = weq 797  ∃!weu 1007

This theorem is referenced by:  cbveu 1018  bireua 1319  2reuswap 1341  euxfr2 1435  euxfr 1436  euuni 1954  funeu2 2686  dffun7 2688  fneu2 2729  fnopabg 2745  tz6.12 2843  fvopab2 2878  fsn 2895  aceq5lem1 3558  aceq5lem5 3562  zmin 4617

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-gen 677  ax-9 799  ax-12 802  ax-17 925

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

metamath.org