Theorem dfcleq 2169

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

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

This theorem was proved from axioms:  ax-ext 2157

This theorem depends on definitions:  df-cleq 2168

This theorem is referenced by:  cvjust  2170  eqriv  2172  eqrdv  2173  eqcom  2177  eqeq1  2182  eleq2  2239  cleqh  2275  abbi  2289  nfeq  2325  nfeqd  2332  cleqf  2342  eqss  3168  ddifstab  3265  ssequn1  3303  eqv  3440  disj3  3473  undif4  3483  vnex  4129  inex1  4132  zfpair2  4204  sucel  4404  uniex2  4430  bj-vprc  14208  bdinex1  14211  bj-zfpair2  14222  bj-uniex2  14228