Theorem dfcleq 2223

Description: The same as df-cleq 2222 with the hypothesis removed using the Axiom of Extensionality ax-ext 2211. (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 2211	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑧) → 𝑦 = 𝑧)
2	1	df-cleq 2222	1 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))

Syntax hints:   ↔ wb 105  ∀wal 1393   = wceq 1395   ∈ wcel 2200

This theorem was proved from axioms:  ax-ext 2211

This theorem depends on definitions:  df-cleq 2222

This theorem is referenced by:  cvjust  2224  eqriv  2226  eqrdv  2227  eqcom  2231  eqeq1  2236  eleq2  2293  cleqh  2329  abbi  2343  nfeq  2380  nfeqd  2387  cleqf  2397  eqss  3240  ddifstab  3337  ssequn1  3375  eqv  3512  disj3  3545  undif4  3555  vnex  4218  inex1  4221  zfpair2  4298  sucel  4505  uniex2  4531  bj-vprc  16441  bdinex1  16444  bj-zfpair2  16455  bj-uniex2  16461