Theorem eubii 1364

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

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

This theorem is referenced by:  cbveu 1368  2eu7 1432  2eu8 1433  reubiia 1757  euxfr2 1897  euxfr 1898  2reuswap 1908  reuun2 2249  zfnuleu 2675  0ex 2679  snex 2718  euuni 2844  funeu2 3479  dffun7 3481  funcnv3 3498  fneu2 3533  fnopabg 3555  tz6.12 3676  fvopab2 3730  fsn 3773  aceq5lem1 4659  aceq5lem5 4663  zmin 6118  climreu 6989  isumclimtf 7082

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-gen 955  ax-9 1102  ax-12 1104  ax-17 1190

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 957  df-eu 1359

Copyright terms: Public domain