Theorem dfcleq 2075

Description: The same as df-cleq 2074 with the hypothesis removed using the Axiom of Extensionality ax-ext 2063. (Contributed by NM, 15-Sep-1993.)

Assertion

Ref	Expression
dfcleq	|- ( A = B <-> A. x ( x e. A <-> x e. B ) )

Distinct variable groups:   x, A   x, B

Proof of Theorem dfcleq

Dummy variables y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ax-ext 2063	. 2 |- ( A. x ( x e. y <-> x e. z ) -> y = z )
2	1	df-cleq 2074	1 |- ( A = B <-> A. x ( x e. A <-> x e. B ) )

Syntax hints:   <-> wb 103   A.wal 1282   = wceq 1284   e. wcel 1433

This theorem was proved from axioms:  ax-ext 2063

This theorem depends on definitions:  df-cleq 2074

This theorem is referenced by:  cvjust  2076  eqriv  2078  eqrdv  2079  eqcom  2083  eqeq1  2087  eleq2  2142  cleqh  2178  abbi  2192  nfeq  2226  nfeqd  2233  cleqf  2242  eqss  3014  ddifstab  3104  ssequn1  3142  eqv  3267  disj3  3296  undif4  3306  vprc  3909  inex1  3912  zfpair2  3965  sucel  4165  uniex2  4191  bj-vprc  10687  bdinex1  10690  bj-zfpair2  10701  bj-uniex2  10707