Theorem moeq 1920

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 1814	. . . 4 |- (A e. V <-> E.x x = A)
2		eueq 1916	. . . 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 1383	. 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 956   e. wcel 958  E.wex 980  E!weu 1380  E*wmo 1381  Vcvv 1811

This theorem is referenced by:  mosub 1922  euxfr2 1926  reuxfr2 2903  funopabeq 3549  opabex2 3610  opabex2g 3611  fconst 3658  fvex 3732  fvopab4g 3779  oprabex2g 4020  oprabex3 4022  oprabval2gf 4026  oprabval3 4030  oprabval6g 4032  2ndconst 4097  axaddopr 5265  axmulopr 5266  spwval2 8653

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-11 967  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812

Copyright terms: Public domain