Theorem dfcleq 2187

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

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

This theorem was proved from axioms:  ax-ext 2175

This theorem depends on definitions:  df-cleq 2186

This theorem is referenced by:  cvjust  2188  eqriv  2190  eqrdv  2191  eqcom  2195  eqeq1  2200  eleq2  2257  cleqh  2293  abbi  2307  nfeq  2344  nfeqd  2351  cleqf  2361  eqss  3195  ddifstab  3292  ssequn1  3330  eqv  3467  disj3  3500  undif4  3510  vnex  4161  inex1  4164  zfpair2  4240  sucel  4442  uniex2  4468  bj-vprc  15458  bdinex1  15461  bj-zfpair2  15472  bj-uniex2  15478