Theorem dfcleq 2183

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

Syntax hints:   ↔ wb 105  ∀wal 1362   = wceq 1364   ∈ wcel 2160

This theorem was proved from axioms:  ax-ext 2171

This theorem depends on definitions:  df-cleq 2182

This theorem is referenced by:  cvjust  2184  eqriv  2186  eqrdv  2187  eqcom  2191  eqeq1  2196  eleq2  2253  cleqh  2289  abbi  2303  nfeq  2340  nfeqd  2347  cleqf  2357  eqss  3185  ddifstab  3282  ssequn1  3320  eqv  3457  disj3  3490  undif4  3500  vnex  4149  inex1  4152  zfpair2  4228  sucel  4428  uniex2  4454  bj-vprc  15101  bdinex1  15104  bj-zfpair2  15115  bj-uniex2  15121