Theorem dfcleq 2158

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

Syntax hints:   ↔ wb 104  ∀wal 1340   = wceq 1342   ∈ wcel 2135

This theorem was proved from axioms:  ax-ext 2146

This theorem depends on definitions:  df-cleq 2157

This theorem is referenced by:  cvjust  2159  eqriv  2161  eqrdv  2162  eqcom  2166  eqeq1  2171  eleq2  2228  cleqh  2264  abbi  2278  nfeq  2314  nfeqd  2321  cleqf  2331  eqss  3152  ddifstab  3249  ssequn1  3287  eqv  3423  disj3  3456  undif4  3466  vnex  4107  inex1  4110  zfpair2  4182  sucel  4382  uniex2  4408  bj-vprc  13613  bdinex1  13616  bj-zfpair2  13627  bj-uniex2  13633