Theorem moeq 2863

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 2695	. . . 4 |- ( A e. _V <-> E. x x = A )
2		eueq 2859	. . . 4 |- ( A e. _V <-> E! x x = A )
3	1, 2	bitr3i 185	. . 3 |- ( E. x x = A <-> E! x x = A )
4	3	biimpi 119	. 2 |- ( E. x x = A -> E! x x = A )
5		df-mo 2004	. 2 |- ( E* x x = A <-> ( E. x x = A -> E! x x = A ) )
6	4, 5	mpbir 145	1 |- E* x x = A

Syntax hints:   -> wi 4   = wceq 1332   E.wex 1469   e. wcel 1481   E!weu 2000   E*wmo 2001   _Vcvv 2689

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-v 2691

This theorem is referenced by:  euxfr2dc  2873  reueq  2887  mosn  3567  sndisj  3933  disjxsn  3935  reusv1  4387  funopabeq  5167  funcnvsn  5176  fvmptg  5505  fvopab6  5525  ovmpt4g  5901  ovi3  5915  ov6g  5916  oprabex3  6035  1stconst  6126  2ndconst  6127  axaddf  7700  axmulf  7701