Theorem dfcleq 2190

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

Syntax hints:   <-> wb 105   A.wal 1362   = wceq 1364   e. wcel 2167

This theorem was proved from axioms:  ax-ext 2178

This theorem depends on definitions:  df-cleq 2189

This theorem is referenced by:  cvjust  2191  eqriv  2193  eqrdv  2194  eqcom  2198  eqeq1  2203  eleq2  2260  cleqh  2296  abbi  2310  nfeq  2347  nfeqd  2354  cleqf  2364  eqss  3199  ddifstab  3296  ssequn1  3334  eqv  3471  disj3  3504  undif4  3514  vnex  4165  inex1  4168  zfpair2  4244  sucel  4446  uniex2  4472  bj-vprc  15626  bdinex1  15629  bj-zfpair2  15640  bj-uniex2  15646