Theorem dfcleq 2190

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

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

This theorem was proved from axioms:  ax-ext 2178

This theorem depends on definitions:  df-cleq 2189

This theorem is referenced by:  cvjust  2191  eqriv  2193  eqrdv  2194  eqcom  2198  eqeq1  2203  eleq2  2260  cleqh  2296  abbi  2310  nfeq  2347  nfeqd  2354  cleqf  2364  eqss  3198  ddifstab  3295  ssequn1  3333  eqv  3470  disj3  3503  undif4  3513  vnex  4164  inex1  4167  zfpair2  4243  sucel  4445  uniex2  4471  bj-vprc  15542  bdinex1  15545  bj-zfpair2  15556  bj-uniex2  15562