Theorem dfcleq 2159

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

Syntax hints:   ↔ wb 104  ∀wal 1341   = wceq 1343   ∈ wcel 2136

This theorem was proved from axioms:  ax-ext 2147

This theorem depends on definitions:  df-cleq 2158

This theorem is referenced by:  cvjust  2160  eqriv  2162  eqrdv  2163  eqcom  2167  eqeq1  2172  eleq2  2230  cleqh  2266  abbi  2280  nfeq  2316  nfeqd  2323  cleqf  2333  eqss  3157  ddifstab  3254  ssequn1  3292  eqv  3428  disj3  3461  undif4  3471  vnex  4113  inex1  4116  zfpair2  4188  sucel  4388  uniex2  4414  bj-vprc  13778  bdinex1  13781  bj-zfpair2  13792  bj-uniex2  13798