Theorem moeq 3247

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 3085	. . . 4 |- ( A e. _V <-> E. x x = A )
2		eueq 3243	. . . 4 |- ( A e. _V <-> E! x x = A )
3	1, 2	bitr3i 254	. . 3 |- ( E. x x = A <-> E! x x = A )
4	3	biimpi 197	. 2 |- ( E. x x = A -> E! x x = A )
5		df-mo 2270	. 2 |- ( E* x x = A <-> ( E. x x = A -> E! x x = A ) )
6	4, 5	mpbir 212	1 |- E* x x = A

Syntax hints:   -> wi 4   = wceq 1437   E.wex 1659   e. wcel 1868   E!weu 2265   E*wmo 2266   _Vcvv 3081

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-v 3083

This theorem is referenced by:  mosub  3249  euxfr2  3256  reueq  3269  sndisj  4412  disjxsn  4414  reusv1  4620  reusv2lem1  4621  reuxfr2d  4640  funopabeq  5631  funcnvsn  5642  fvmptg  5958  fvopab6  5986  ovmpt4g  6429  ov3  6443  ov6g  6444  oprabex3  6792  1stconst  6891  2ndconst  6892  iunmapdisj  8454  axaddf  9569  axmulf  9570  joinfval  16232  joinval  16236  meetfval  16246  meetval  16250  reuxfr3d  28108  abrexdom2jm  28126  abrexdom2  31969