Theorem dfcleq 2171

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

Syntax hints:   ↔ wb 105  ∀wal 1351   = wceq 1353   ∈ wcel 2148

This theorem was proved from axioms:  ax-ext 2159

This theorem depends on definitions:  df-cleq 2170

This theorem is referenced by:  cvjust  2172  eqriv  2174  eqrdv  2175  eqcom  2179  eqeq1  2184  eleq2  2241  cleqh  2277  abbi  2291  nfeq  2327  nfeqd  2334  cleqf  2344  eqss  3172  ddifstab  3269  ssequn1  3307  eqv  3444  disj3  3477  undif4  3487  vnex  4136  inex1  4139  zfpair2  4212  sucel  4412  uniex2  4438  bj-vprc  14733  bdinex1  14736  bj-zfpair2  14747  bj-uniex2  14753