Theorem dfcleq 2226

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

Syntax hints:   <-> wb 105   A.wal 1396   = wceq 1398   e. wcel 2203

This theorem was proved from axioms:  ax-ext 2214

This theorem depends on definitions:  df-cleq 2225

This theorem is referenced by:  cvjust  2227  eqriv  2229  eqrdv  2230  eqcom  2234  eqeq1  2239  eleq2  2296  cleqh  2332  abbibcom  2346  abbib  2350  nfeq  2392  nfeqd  2399  cleqf  2409  eqss  3253  ddifstab  3351  ssequn1  3389  eqv  3528  disj3  3561  undif4  3571  vnex  4241  inex1  4244  zfpair2  4323  sucel  4531  uniex2  4557  bj-vprc  16666  bdinex1  16669  bj-zfpair2  16680  bj-uniex2  16686