Theorem eubii 1420

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

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

This theorem is referenced by:  cbveu 1424  2eu7 1489  2eu8 1490  reubiia 1819  euxfr2 1964  euxfr 1965  2reuswap 1975  reuun2 2322  zfnuleu 2758  0ex 2762  snex 2802  euuni 2936  funeu2 3613  dffun8 3615  funcnv3 3633  fneu2 3668  fnopabg 3690  tz6.12 3813  fvopab2 3867  fsn 3910  aceq5lem1 4821  aceq5lem5 4825  zmin 6332  climreu 7224  isumclimtfi 7318

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 995  ax-12 1000  ax-17 1003  ax-4 1005  ax-5o 1007  ax-6o 1010  ax-9o 1155

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1013  df-eu 1415

Copyright terms: Public domain