Theorem dfcleq 2034

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

Syntax hints:   ↔ wb 98  ∀wal 1241   = wceq 1243   ∈ wcel 1393

This theorem was proved from axioms:  ax-ext 2022

This theorem depends on definitions:  df-cleq 2033

This theorem is referenced by:  cvjust  2035  eqriv  2037  eqrdv  2038  eqcom  2042  eqeq1  2046  eleq2  2101  cleqh  2137  abbi  2151  nfeq  2185  nfeqd  2192  cleqf  2201  eqss  2960  ssequn1  3113  eqv  3240  disj3  3272  undif4  3284  vprc  3888  inex1  3891  zfpair2  3945  sucel  4147  uniex2  4173  bj-vprc  10016  bdinex1  10019  bj-zfpair2  10030  bj-uniex2  10036