Theorem dfcleq 2225

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

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

This theorem was proved from axioms:  ax-ext 2213

This theorem depends on definitions:  df-cleq 2224

This theorem is referenced by:  cvjust  2226  eqriv  2228  eqrdv  2229  eqcom  2233  eqeq1  2238  eleq2  2295  cleqh  2331  abbi  2345  abbib  2349  nfeq  2383  nfeqd  2390  cleqf  2400  eqss  3243  ddifstab  3341  ssequn1  3379  eqv  3516  disj3  3549  undif4  3559  vnex  4225  inex1  4228  zfpair2  4306  sucel  4513  uniex2  4539  bj-vprc  16592  bdinex1  16595  bj-zfpair2  16606  bj-uniex2  16612