Theorem eubii 1380

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

Hypothesis

Ref	Expression
eubii.1	|- (ph <-> ps)

Assertion

Ref	Expression
eubii	|- (E!xph <-> E!xps)

Proof of Theorem eubii

Step	Hyp	Ref	Expression
1		equid 1122	. 2 |- x = x
2		hbequid 1165	. . 3 |- (x = x -> A.x x = x)
3		eubii.1	. . . 4 |- (ph <-> ps)
4	3	a1i 8	. . 3 |- (x = x -> (ph <-> ps))
5	2, 4	eubid 1378	. 2 |- (x = x -> (E!xph <-> E!xps))
6	1, 5	ax-mp 7	1 |- (E!xph <-> E!xps)

Syntax hints:   <-> wb 146  E!weu 1373

This theorem is referenced by:  cbveu 1384  2eu7 1448  2eu8 1449  reubiia 1773  euxfr2 1916  euxfr 1917  2reuswap 1927  reuun2 2268  zfnuleu 2697  0ex 2701  snex 2740  euuni 2871  funeu2 3524  dffun7 3526  funcnv3 3544  fneu2 3579  fnopabg 3601  tz6.12 3722  fvopab2 3776  fsn 3819  aceq5lem1 4707  aceq5lem5 4711  zmin 6167  climreu 7038  isumclimtf 7131

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-eu 1375

Copyright terms: Public domain