Theorem dfcleq 2171

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

Syntax hints:   <-> wb 105   A.wal 1351   = wceq 1353   e. wcel 2148

This theorem was proved from axioms:  ax-ext 2159

This theorem depends on definitions:  df-cleq 2170

This theorem is referenced by:  cvjust  2172  eqriv  2174  eqrdv  2175  eqcom  2179  eqeq1  2184  eleq2  2241  cleqh  2277  abbi  2291  nfeq  2327  nfeqd  2334  cleqf  2344  eqss  3171  ddifstab  3268  ssequn1  3306  eqv  3443  disj3  3476  undif4  3486  vnex  4135  inex1  4138  zfpair2  4211  sucel  4411  uniex2  4437  bj-vprc  14651  bdinex1  14654  bj-zfpair2  14665  bj-uniex2  14671