Theorem dfcleq 2228

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

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

This theorem was proved from axioms:  ax-ext 2216

This theorem depends on definitions:  df-cleq 2227

This theorem is referenced by:  cvjust  2229  eqriv  2231  eqrdv  2232  eqcom  2236  eqeq1  2241  eleq2  2298  cleqh  2334  abbibcom  2348  abbib  2352  nfeq  2394  nfeqd  2401  cleqf  2411  eqss  3257  ddifstab  3355  ssequn1  3393  eqv  3532  disj3  3565  undif4  3575  vnex  4246  inex1  4249  zfpair2  4328  sucel  4536  uniex2  4562  bj-vprc  16778  bdinex1  16781  bj-zfpair2  16792  bj-uniex2  16798