Theorem moeq 3229

Description: There is at most one set equal to a class. (Contributed by NM, 8-Mar-1995.)

Assertion

Ref	Expression
moeq	|- E* x x = A

Distinct variable group:   x, A

Proof of Theorem moeq

Step	Hyp	Ref	Expression
1		isset 3069	. . . 4 |- ( A e. _V <-> E. x x = A )
2		eueq 3225	. . . 4 |- ( A e. _V <-> E! x x = A )
3	1, 2	bitr3i 251	. . 3 |- ( E. x x = A <-> E! x x = A )
4	3	biimpi 194	. 2 |- ( E. x x = A -> E! x x = A )
5		df-mo 2265	. 2 |- ( E* x x = A <-> ( E. x x = A -> E! x x = A ) )
6	4, 5	mpbir 209	1 |- E* x x = A

Syntax hints:   -> wi 4   = wceq 1370   E.wex 1587   e. wcel 1758   E!weu 2260   E*wmo 2261   _Vcvv 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-v 3067

This theorem is referenced by:  mosub  3231  euxfr2  3238  reueq  3251  sndisj  4379  disjxsn  4381  reusv1  4587  reusv2lem1  4588  reuxfr2d  4610  funopabeq  5547  funcnvsn  5558  fvmptg  5868  fvopab6  5892  ovmpt4g  6310  ov3  6324  ov6g  6325  oprabex3  6663  1stconst  6758  2ndconst  6759  iunmapdisj  8291  axaddf  9410  axmulf  9411  joinfval  15270  joinval  15274  meetfval  15284  meetval  15288  reuxfr3d  26005  abrexdom2jm  26021  abrexdom2  28760