Theorem dfcleq 2199

Description: The same as df-cleq 2198 with the hypothesis removed using the Axiom of Extensionality ax-ext 2187. (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 2187	. 2 |- ( A. x ( x e. y <-> x e. z ) -> y = z )
2	1	df-cleq 2198	1 |- ( A = B <-> A. x ( x e. A <-> x e. B ) )

Syntax hints:   <-> wb 105   A.wal 1371   = wceq 1373   e. wcel 2176

This theorem was proved from axioms:  ax-ext 2187

This theorem depends on definitions:  df-cleq 2198

This theorem is referenced by:  cvjust  2200  eqriv  2202  eqrdv  2203  eqcom  2207  eqeq1  2212  eleq2  2269  cleqh  2305  abbi  2319  nfeq  2356  nfeqd  2363  cleqf  2373  eqss  3208  ddifstab  3305  ssequn1  3343  eqv  3480  disj3  3513  undif4  3523  vnex  4175  inex1  4178  zfpair2  4254  sucel  4457  uniex2  4483  bj-vprc  15832  bdinex1  15835  bj-zfpair2  15846  bj-uniex2  15852