Theorem dfcleq 2094

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

Syntax hints:   ↔ wb 104  ∀wal 1297   = wceq 1299   ∈ wcel 1448

This theorem was proved from axioms:  ax-ext 2082

This theorem depends on definitions:  df-cleq 2093

This theorem is referenced by:  cvjust  2095  eqriv  2097  eqrdv  2098  eqcom  2102  eqeq1  2106  eleq2  2163  cleqh  2199  abbi  2213  nfeq  2248  nfeqd  2255  cleqf  2264  eqss  3062  ddifstab  3155  ssequn1  3193  eqv  3329  disj3  3362  undif4  3372  vnex  3999  inex1  4002  zfpair2  4070  sucel  4270  uniex2  4296  bj-vprc  12675  bdinex1  12678  bj-zfpair2  12689  bj-uniex2  12695