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  2463  nfeq  2496  nfeqd  2503  cleqf  2513  dfss2  3262  eqss  3287  ssequn1  3433  necompl  3544  eqv  3565  disj3  3595  undif4  3607  axprimlem1  4088  axprimlem2  4089  ninexg  4097  1cex  4142  pw111  4170  opkelimagekg  4271  xpkvexg  4285  p6exg  4290  dfaddc2  4381  nnsucelrlem1  4424  ltfinex  4464  eqtfinrelk  4486  evenfinex  4503  oddfinex  4504  evenodddisjlem1  4515  nnadjoinlem1  4519  dfop2lem1  4573  eqop  4611  setconslem2  4732  dfswap2  4741  brimage  5793  releqel  5807  releqmpt2  5809  qsexg  5982