Theorem moeq 3226

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 3061	. . . 4 |- ( A e. _V <-> E. x x = A )
2		eueq 3222	. . . 4 |- ( A e. _V <-> E! x x = A )
3	1, 2	bitr3i 259	. . 3 |- ( E. x x = A <-> E! x x = A )
4	3	biimpi 199	. 2 |- ( E. x x = A -> E! x x = A )
5		df-mo 2315	. 2 |- ( E* x x = A <-> ( E. x x = A -> E! x x = A ) )
6	4, 5	mpbir 214	1 |- E* x x = A

Syntax hints:   -> wi 4   = wceq 1455   E.wex 1674   e. wcel 1898   E!weu 2310   E*wmo 2311   _Vcvv 3057

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-v 3059

This theorem is referenced by:  mosub  3228  euxfr2  3235  reueq  3248  rmoeq  3249  sndisj  4410  disjxsn  4412  reusv1  4620  reusv2lem1  4621  reuxfr2d  4640  funopabeq  5639  funcnvsn  5650  fvmptg  5974  fvopab6  6003  ovmpt4g  6451  ov3  6465  ov6g  6466  oprabex3  6814  1stconst  6916  2ndconst  6917  iunmapdisj  8485  axaddf  9600  axmulf  9601  joinfval  16302  joinval  16306  meetfval  16316  meetval  16320  reuxfr3d  28181  abrexdom2jm  28198  abrexdom2  32104