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 ) )

This proof depends on syntax axioms:   <-> wb 105   A.wal 1400   = wceq 1402   e. wcel 2209

This proof depends on axioms:  ax-ext 2220

This proof depends on definitions:  df-cleq 2231

This theorem is used 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  3577  undif4  3587  vnex  4264  inex1  4267  zfpair2  4347  sucel  4555  uniex2  4581  uniex2OLD  4582  bj-vprc  16922  bdinex1  16925  bj-zfpair2  16936  bj-uniex2  16942