Theorem dfcleq 2164

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

Syntax hints:   ↔ wb 104  ∀wal 1346   = wceq 1348   ∈ wcel 2141

This theorem was proved from axioms:  ax-ext 2152

This theorem depends on definitions:  df-cleq 2163

This theorem is referenced by:  cvjust  2165  eqriv  2167  eqrdv  2168  eqcom  2172  eqeq1  2177  eleq2  2234  cleqh  2270  abbi  2284  nfeq  2320  nfeqd  2327  cleqf  2337  eqss  3162  ddifstab  3259  ssequn1  3297  eqv  3434  disj3  3467  undif4  3477  vnex  4120  inex1  4123  zfpair2  4195  sucel  4395  uniex2  4421  bj-vprc  13931  bdinex1  13934  bj-zfpair2  13945  bj-uniex2  13951