Theorem dfcleq 2133

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

Syntax hints:   ↔ wb 104  ∀wal 1329   = wceq 1331   ∈ wcel 1480

This theorem was proved from axioms:  ax-ext 2121

This theorem depends on definitions:  df-cleq 2132

This theorem is referenced by:  cvjust  2134  eqriv  2136  eqrdv  2137  eqcom  2141  eqeq1  2146  eleq2  2203  cleqh  2239  abbi  2253  nfeq  2289  nfeqd  2296  cleqf  2305  eqss  3112  ddifstab  3208  ssequn1  3246  eqv  3382  disj3  3415  undif4  3425  vnex  4059  inex1  4062  zfpair2  4132  sucel  4332  uniex2  4358  bj-vprc  13094  bdinex1  13097  bj-zfpair2  13108  bj-uniex2  13114