Theorem dfcleq 2201

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

Syntax hints:   <-> wb 105   A.wal 1371   = wceq 1373   e. wcel 2178

This theorem was proved from axioms:  ax-ext 2189

This theorem depends on definitions:  df-cleq 2200

This theorem is referenced by:  cvjust  2202  eqriv  2204  eqrdv  2205  eqcom  2209  eqeq1  2214  eleq2  2271  cleqh  2307  abbi  2321  nfeq  2358  nfeqd  2365  cleqf  2375  eqss  3216  ddifstab  3313  ssequn1  3351  eqv  3488  disj3  3521  undif4  3531  vnex  4191  inex1  4194  zfpair2  4270  sucel  4475  uniex2  4501  bj-vprc  16031  bdinex1  16034  bj-zfpair2  16045  bj-uniex2  16051