Theorem dfcleq 2079

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

Syntax hints:   ↔ wb 103  ∀wal 1285   = wceq 1287   ∈ wcel 1436

This theorem was proved from axioms:  ax-ext 2067

This theorem depends on definitions:  df-cleq 2078

This theorem is referenced by:  cvjust  2080  eqriv  2082  eqrdv  2083  eqcom  2087  eqeq1  2091  eleq2  2148  cleqh  2184  abbi  2198  nfeq  2232  nfeqd  2239  cleqf  2248  eqss  3029  ddifstab  3121  ssequn1  3159  eqv  3291  disj3  3323  undif4  3333  vnex  3945  inex1  3948  zfpair2  4011  sucel  4211  uniex2  4237  bj-vprc  11232  bdinex1  11235  bj-zfpair2  11246  bj-uniex2  11252