Theorem dfcleq 2187

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

Syntax hints:   ↔ wb 105  ∀wal 1362   = wceq 1364   ∈ wcel 2164

This theorem was proved from axioms:  ax-ext 2175

This theorem depends on definitions:  df-cleq 2186

This theorem is referenced by:  cvjust  2188  eqriv  2190  eqrdv  2191  eqcom  2195  eqeq1  2200  eleq2  2257  cleqh  2293  abbi  2307  nfeq  2344  nfeqd  2351  cleqf  2361  eqss  3194  ddifstab  3291  ssequn1  3329  eqv  3466  disj3  3499  undif4  3509  vnex  4160  inex1  4163  zfpair2  4239  sucel  4441  uniex2  4467  bj-vprc  15388  bdinex1  15391  bj-zfpair2  15402  bj-uniex2  15408