Theorem moeq 2955

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 2783	. . . 4 |- ( A e. _V <-> E. x x = A )
2		eueq 2951	. . . 4 |- ( A e. _V <-> E! x x = A )
3	1, 2	bitr3i 186	. . 3 |- ( E. x x = A <-> E! x x = A )
4	3	biimpi 120	. 2 |- ( E. x x = A -> E! x x = A )
5		df-mo 2059	. 2 |- ( E* x x = A <-> ( E. x x = A -> E! x x = A ) )
6	4, 5	mpbir 146	1 |- E* x x = A

Syntax hints:   -> wi 4   = wceq 1373   E.wex 1516   E!weu 2055   E*wmo 2056   e. wcel 2178   _Vcvv 2776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2194  df-cleq 2200  df-clel 2203  df-v 2778

This theorem is referenced by:  euxfr2dc  2965  reueq  2979  mosn  3679  sndisj  4055  disjxsn  4057  reusv1  4523  funopabeq  5326  funcnvsn  5338  fvmptg  5678  fvopab6  5699  ovmpt4g  6091  ovi3  6106  ov6g  6107  oprabex3  6237  1stconst  6330  2ndconst  6331  axaddf  8016  axmulf  8017