Theorem dfcleq 1463

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

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 1452	. 2 |- (A.x(x e. y <-> x e. z) -> y = z)
2	1	df-cleq 1462	1 |- (A = B <-> A.x(x e. A <-> x e. B))

Syntax hints:   <-> wb 146  A.wal 951   = wceq 953   e. wcel 955

This theorem is referenced by:  cvjust 1464  eqrdv 1466  eqriv 1467  eqcom 1469  eqeq1 1473  eleq2 1527  cleqf 1552  hbeq 1557  sbcel12g 2001  sbceqdig 2002  eqss 2067  eqv 2285  disj3 2304  undif4 2315  nvelv 2703  inex1 2706  axpr 2768  zfpair2 2770  uniex2 2860  sucel 3032  dmcosseq 3349  fv2 3705  ntreq0 7650

This theorem was proved from axioms:  ax-ext 1452

This theorem depends on definitions:  df-cleq 1462

Copyright terms: Public domain