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  3239  ddifstab  3336  ssequn1  3374  eqv  3511  disj3  3544  undif4  3554  vnex  4214  inex1  4217  zfpair2  4293  sucel  4498  uniex2  4524  bj-vprc  16189  bdinex1  16192  bj-zfpair2  16203  bj-uniex2  16209