Theorem dfcleq 2226

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

Assertion

Ref	Expression
dfcleq	⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem dfcleq

Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ax-ext 2214	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑧) → 𝑦 = 𝑧)
2	1	df-cleq 2225	1 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))

Syntax hints:   ↔ wb 105  ∀wal 1396   = wceq 1398   ∈ wcel 2203

This theorem was proved from axioms:  ax-ext 2214

This theorem depends on definitions:  df-cleq 2225

This theorem is referenced by:  cvjust  2227  eqriv  2229  eqrdv  2230  eqcom  2234  eqeq1  2239  eleq2  2296  cleqh  2332  abbibcom  2346  abbib  2350  nfeq  2392  nfeqd  2399  cleqf  2409  eqss  3252  ddifstab  3350  ssequn1  3388  eqv  3527  disj3  3560  undif4  3570  vnex  4240  inex1  4243  zfpair2  4322  sucel  4530  uniex2  4556  bj-vprc  16658  bdinex1  16661  bj-zfpair2  16672  bj-uniex2  16678