Theorem eubii 1426

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 1162	. 2 |- x = x
2		hbequid 1206	. . 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 1424	. 2 |- (x = x -> (E!xph <-> E!xps))
6	1, 5	ax-mp 7	1 |- (E!xph <-> E!xps)

Syntax hints:   <-> wb 144  E!weu 1419

This theorem is referenced by:  cbveu 1430  2eu7 1495  2eu8 1496  reubiia 1827  euxfr2 1972  euxfr 1973  2reuswap 1983  reuun2 2330  zfnuleu 2781  0ex 2785  snex 2826  euuni 3105  funeu2 3643  dffun8 3645  funcnv3 3663  fneu2 3699  fnopabg 3722  tz6.12 3848  fvopab2 3902  fsn 3948  aceq5lem1 4881  aceq5lem5 4885  zmin 6391  climreu 7304  isumclimtfi 7399

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 999  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-eu 1421

Copyright terms: Public domain