Theorem dfcleq 2131

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

Syntax hints:   <-> wb 104   A.wal 1329   = wceq 1331   e. wcel 1480

This theorem was proved from axioms:  ax-ext 2119

This theorem depends on definitions:  df-cleq 2130

This theorem is referenced by:  cvjust  2132  eqriv  2134  eqrdv  2135  eqcom  2139  eqeq1  2144  eleq2  2201  cleqh  2237  abbi  2251  nfeq  2287  nfeqd  2294  cleqf  2303  eqss  3107  ddifstab  3203  ssequn1  3241  eqv  3377  disj3  3410  undif4  3420  vnex  4054  inex1  4057  zfpair2  4127  sucel  4327  uniex2  4353  bj-vprc  13083  bdinex1  13086  bj-zfpair2  13097  bj-uniex2  13103