Theorem dfcleq 2200

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

Syntax hints:   ↔ wb 105  ∀wal 1371   = wceq 1373   ∈ wcel 2177

This theorem was proved from axioms:  ax-ext 2188

This theorem depends on definitions:  df-cleq 2199

This theorem is referenced by:  cvjust  2201  eqriv  2203  eqrdv  2204  eqcom  2208  eqeq1  2213  eleq2  2270  cleqh  2306  abbi  2320  nfeq  2357  nfeqd  2364  cleqf  2374  eqss  3212  ddifstab  3309  ssequn1  3347  eqv  3484  disj3  3517  undif4  3527  vnex  4182  inex1  4185  zfpair2  4261  sucel  4464  uniex2  4490  bj-vprc  15966  bdinex1  15969  bj-zfpair2  15980  bj-uniex2  15986