Theorem dfcleq 2232

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

Syntax hints:   ↔ wb 105  ∀wal 1400   = wceq 1402   ∈ wcel 2209

This theorem was proved from axioms:  ax-ext 2220

This theorem depends on definitions:  df-cleq 2231

This theorem is referenced by:  cvjust  2233  eqriv  2235  eqrdv  2236  eqcom  2240  eqeq1  2245  eleq2  2302  cleqh  2338  abbibcom  2352  abbib  2356  nfeq  2400  nfeqd  2407  cleqf  2417  eqss  3263  ddifstab  3361  ssequn1  3399  eqv  3541  disj3  3577  undif4  3587  vnex  4262  inex1  4265  zfpair2  4345  sucel  4553  uniex2  4579  uniex2OLD  4580  bj-vprc  16905  bdinex1  16908  bj-zfpair2  16919  bj-uniex2  16925