Theorem dfcleq 2645

Description: The same as df-cleq 2644 with the hypothesis removed using the Axiom of Extensionality ax-ext 2631. (Contributed by NM, 15-Sep-1993.) Revised to make use of axext3 2633 instead of ax-ext 2631, so that ax-9 2039 will appear in lists of axioms used by a proof, since df-cleq 2644 implies ax-9 2039 by theorem bj-ax9 33015. We may revisit this in the future. (Revised by NM, 28-Oct-2021.) (Proof modification is discouraged.)

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		axext3 2633	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑧) → 𝑦 = 𝑧)
2	1	df-cleq 2644	1 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))

Syntax hints:   ↔ wb 196  ∀wal 1521   = wceq 1523   ∈ wcel 2030

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644

This theorem is referenced by:  cvjust  2646  eqriv  2648  eqrdv  2649  eqeq1d  2653  eqeq1dALT  2654  eleq2d  2716  eleq2dALT  2717  cleqh  2753  nfeqd  2801  eqss  3651  ssequn1  3816  disj3  4054  undif4  4068  vprc  4829  inex1  4832  axpr  4935  zfpair2  4937  sucel  5836  uniex2  6994  brtxpsd3  32128  hfext  32415  onsuct0  32565  bj-abbi  32900  eliminable2a  32966  eliminable2b  32967  eliminable2c  32968  bj-df-cleq  33018  bj-sbeq  33021  bj-sbceqgALT  33022  bj-snsetex  33076  bj-df-v  33141  cover2  33638  releccnveq  34163  rp-fakeinunass  38178  intimag  38265  relexp0eq  38310  ntrneik4w  38715  undif3VD  39432  rnmptpr  39672  uzinico  40105  dvnmul  40476  dvnprodlem3  40481  sge00  40911  sge0resplit  40941  sge0fodjrnlem  40951  hspdifhsp  41151  smfresal  41316