Theorem dfcleq 1098

Description: The same as df-cleq 1097 with the hypothesis removed using the Axiom of Extensionality ax-ext 1074.

Assertion

Ref	Expression
dfcleq	|- (A = B <-> A.x(x e. A <-> x e. B))

Distinct variable group(s):   x,A   x,B

Proof of Theorem dfcleq

Step	Hyp	Ref	Expression
1		ax-ext 1074	. 2 |- (A.x(x e. y <-> x e. z) -> y = z)
2	1	df-cleq 1097	1 |- (A = B <-> A.x(x e. A <-> x e. B))

Syntax hints:   <-> wb 127  A.wal 672   = wceq 1091   e. wcel 1092

This theorem is referenced by:  cleqrd 1100  cleqri 1101  cleqcom 1103  cleq1 1107  eleq2 1150  cleqf 1167  hbeq 1171  nvelv 1483  eqss 1516  inex1 1697  disj3 1736  undif4 1744  uniex 1947  sucel 2296  dmcosseq 2572  fv2 2828

This theorem was proved from axioms:  ax-ext 1074

This theorem depends on definitions:  df-cleq 1097

metamath.org