Theorem dfcleq 2223

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

Syntax hints:   <-> wb 105   A.wal 1393   = wceq 1395   e. wcel 2200

This theorem was proved from axioms:  ax-ext 2211

This theorem depends on definitions:  df-cleq 2222

This theorem is referenced by:  cvjust  2224  eqriv  2226  eqrdv  2227  eqcom  2231  eqeq1  2236  eleq2  2293  cleqh  2329  abbi  2343  nfeq  2380  nfeqd  2387  cleqf  2397  eqss  3240  ddifstab  3337  ssequn1  3375  eqv  3512  disj3  3545  undif4  3555  vnex  4216  inex1  4219  zfpair2  4296  sucel  4503  uniex2  4529  bj-vprc  16401  bdinex1  16404  bj-zfpair2  16415  bj-uniex2  16421