Theorem dfcleq 2134

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

Syntax hints:   <-> wb 104   A.wal 1330   = wceq 1332   e. wcel 1481

This theorem was proved from axioms:  ax-ext 2122

This theorem depends on definitions:  df-cleq 2133

This theorem is referenced by:  cvjust  2135  eqriv  2137  eqrdv  2138  eqcom  2142  eqeq1  2147  eleq2  2204  cleqh  2240  abbi  2254  nfeq  2290  nfeqd  2297  cleqf  2306  eqss  3117  ddifstab  3213  ssequn1  3251  eqv  3387  disj3  3420  undif4  3430  vnex  4067  inex1  4070  zfpair2  4140  sucel  4340  uniex2  4366  bj-vprc  13265  bdinex1  13268  bj-zfpair2  13279  bj-uniex2  13285