Theorem dfcleq 2347

Description: The same as df-cleq 2346 with the hypothesis removed using the Axiom of Extensionality ax-ext 2334. (Contributed by NM, 15-Sep-1993.)

Assertion

Ref	Expression
dfcleq	⊢ (A = B ↔ ∀x(x ∈ A ↔ x ∈ 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 2334	. 2 ⊢ (∀x(x ∈ y ↔ x ∈ z) → y = z)
2	1	df-cleq 2346	1 ⊢ (A = B ↔ ∀x(x ∈ A ↔ x ∈ B))

Syntax hints:   ↔ wb 176  ∀wal 1540   = wceq 1642   ∈ wcel 1710

This theorem was proved from axioms:  ax-ext 2334

This theorem depends on definitions:  df-cleq 2346

This theorem is referenced by:  cvjust  2348  eqriv  2350  eqrdv  2351  eqcom  2355  eqeq1  2359  eleq2  2414  cleqh  2450  abbi  2464  nfeq  2497  nfeqd  2504  cleqf  2514  dfss2  3263  eqss  3288  ssequn1  3434  necompl  3545  eqv  3566  disj3  3596  undif4  3608  axprimlem1  4089  axprimlem2  4090  ninexg  4098  1cex  4143  pw111  4171  opkelimagekg  4272  xpkvexg  4286  p6exg  4291  dfaddc2  4382  nnsucelrlem1  4425  ltfinex  4465  eqtfinrelk  4487  evenfinex  4504  oddfinex  4505  evenodddisjlem1  4516  nnadjoinlem1  4520  dfop2lem1  4574  eqop  4612  setconslem2  4733  dfswap2  4742  brimage  5794  releqel  5808  releqmpt2  5810  qsexg  5983