Theorem moeq 1916

Description: There is at most one set equal to a class.

Assertion

Ref	Expression
moeq	|- E*x x = A

Distinct variable group:   x,A

Proof of Theorem moeq

Step	Hyp	Ref	Expression
1		isset 1810	. . . 4 |- (A e. V <-> E.x x = A)
2		eueq 1912	. . . 4 |- (A e. V <-> E!x x = A)
3	1, 2	bitr3 175	. . 3 |- (E.x x = A <-> E!x x = A)
4	3	biimp 151	. 2 |- (E.x x = A -> E!x x = A)
5		df-mo 1381	. 2 |- (E*x x = A <-> (E.x x = A -> E!x x = A))
6	4, 5	mpbir 190	1 |- E*x x = A

Syntax hints:   -> wi 3   = wceq 954   e. wcel 956  E.wex 978  E!weu 1378  E*wmo 1379  Vcvv 1807

This theorem is referenced by:  mosub 1918  euxfr2 1922  reuxfr2 2898  funopabeq 3541  opabex2 3602  opabex2g 3603  fconst 3649  fvex 3723  fvopab4g 3770  oprabex2g 4011  oprabex3 4013  oprabval2gf 4017  oprabval3 4021  oprabval6g 4023  2ndconst 4087  axaddopr 5245  axmulopr 5246  spwval2 8595

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-11 965  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-v 1808

Copyright terms: Public domain