Theorem dfcleq 1468

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

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

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

Syntax hints:   <-> wb 146  A.wal 952   = wceq 954   e. wcel 956

This theorem is referenced by:  cvjust 1469  eqrdv 1471  eqriv 1472  eqcom 1474  eqeq1 1478  eleq2 1532  cleqf 1557  hbeq 1562  sbcel12g 2007  sbceqdig 2008  eqss 2073  eqv 2291  disj3 2310  undif4 2321  nvelv 2708  inex1 2711  axpr 2773  zfpair2 2775  uniex2 2864  sucel 3037  dmcosseq 3357  fv2 3711  ntreq0 7658

This theorem was proved from axioms:  ax-ext 1457

This theorem depends on definitions:  df-cleq 1467

Copyright terms: Public domain