Theorem dfcleq 2232

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

Syntax hints:   <-> wb 105   A.wal 1400   = wceq 1402   e. wcel 2209

This theorem was proved from axioms:  ax-ext 2220

This theorem depends on definitions:  df-cleq 2231

This theorem is referenced by:  cvjust  2233  eqriv  2235  eqrdv  2236  eqcom  2240  eqeq1  2245  eleq2  2302  cleqh  2338  abbibcom  2352  abbib  2356  nfeq  2400  nfeqd  2407  cleqf  2417  eqss  3263  ddifstab  3361  ssequn1  3399  eqv  3541  disj3  3576  undif4  3586  vnex  4259  inex1  4262  zfpair2  4342  sucel  4550  uniex2  4576  uniex2OLD  4577  bj-vprc  16836  bdinex1  16839  bj-zfpair2  16850  bj-uniex2  16856