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 1395   = wceq 1397   ∈ 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  nfeq  2382  nfeqd  2389  cleqf  2399  eqss  3242  ddifstab  3339  ssequn1  3377  eqv  3514  disj3  3547  undif4  3557  vnex  4220  inex1  4223  zfpair2  4300  sucel  4507  uniex2  4533  bj-vprc  16517  bdinex1  16520  bj-zfpair2  16531  bj-uniex2  16537