Theorem dfcleq 2083

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

Syntax hints:   <-> wb 104   A.wal 1288   = wceq 1290   e. wcel 1439

This theorem was proved from axioms:  ax-ext 2071

This theorem depends on definitions:  df-cleq 2082

This theorem is referenced by:  cvjust  2084  eqriv  2086  eqrdv  2087  eqcom  2091  eqeq1  2095  eleq2  2152  cleqh  2188  abbi  2202  nfeq  2237  nfeqd  2244  cleqf  2253  eqss  3041  ddifstab  3133  ssequn1  3171  eqv  3306  disj3  3339  undif4  3349  vnex  3976  inex1  3979  zfpair2  4046  sucel  4246  uniex2  4272  bj-vprc  12060  bdinex1  12063  bj-zfpair2  12074  bj-uniex2  12080