Theorem moeq 3272

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 3110	. . . 4 |- ( A e. _V <-> E. x x = A )
2		eueq 3268	. . . 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 2289	. 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 1398   E.wex 1617   e. wcel 1823   E!weu 2284   E*wmo 2285   _Vcvv 3106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-v 3108

This theorem is referenced by:  mosub  3274  euxfr2  3281  reueq  3294  sndisj  4431  disjxsn  4433  reusv1  4637  reusv2lem1  4638  reuxfr2d  4660  funopabeq  5604  funcnvsn  5615  fvmptg  5929  fvopab6  5956  ovmpt4g  6398  ov3  6412  ov6g  6413  oprabex3  6762  1stconst  6861  2ndconst  6862  iunmapdisj  8395  axaddf  9511  axmulf  9512  joinfval  15830  joinval  15834  meetfval  15844  meetval  15848  reuxfr3d  27586  abrexdom2jm  27605  abrexdom2  30462