Theorem eubii 1780

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 1484	. 2 |- x = x
2		hbequid2 1533	. . 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 1778	. 2 |- (x = x -> (E!xph <-> E!xps))
6	1, 5	ax-mp 7	1 |- (E!xph <-> E!xps)

Syntax hints:   <-> wb 163  E!weu 1771

This theorem is referenced by:  cbveu 1785  2eu7 1859  2eu8 1860  reubiia 2261  cbvreuv 2282  reuv 2307  euxfr2 2437  euxfr 2438  2reuswap 2449  reuun2 2873  zfnuleu 3442  0exOLD 3447  snexOLD 3493  copsexg 3537  euuni 3807  eualeqhb 3824  euexeqOLD 3826  euexaleq 3827  eufromeq2 3829  eufromeq4 3831  eufromeq6 3833  funeu2 4446  dffun8OLD 4449  funcnv3 4476  fneu2 4519  fnopabg 4546  tz6.12 4694  fvopab2 4754  fsn 4807  reiota4 5107  aceq5lem1 5897  aceq5lem5 5901  zmin 7432  climreu 8361  isumclimtfi 8456  bnj80 12442  bnj88 12447  bnj111OLD 12456  bnj863 12796  bnj1331 13062  bnj1366 13091  bnj119 13229  bnj130 13240  bnj207 13248  divalglem10 13705  divalgb 13707  limvinlv 14941  isline1 15294

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-eu 1775

Copyright terms: Public domain