Theorem dfcleq 2615

Description: The same as df-cleq 2614 with the hypothesis removed using the Axiom of Extensionality ax-ext 2601. (Contributed by NM, 15-Sep-1993.) Revised to make use of axext3 2603 instead of ax-ext 2601, so that ax-9 1996 will appear in lists of axioms used by a proof, since df-cleq 2614 implies ax-9 1996 by theorem bj-ax9 32534. 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 2603	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑧) → 𝑦 = 𝑧)
2	1	df-cleq 2614	1 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))

Syntax hints:   ↔ wb 196  ∀wal 1478   = wceq 1480   ∈ wcel 1987

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-ext 2601

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-cleq 2614

This theorem is referenced by:  cvjust  2616  eqriv  2618  eqrdv  2619  eqeq1d  2623  eqeq1dALT  2624  eleq2d  2684  eleq2dALT  2685  cleqh  2721  nfeqd  2768  eqss  3598  ssequn1  3761  disj3  3993  undif4  4007  vprc  4756  inex1  4759  axpr  4866  zfpair2  4868  sucel  5757  uniex2  6905  bnj145OLD  30500  brtxpsd3  31642  hfext  31929  onsuct0  32079  bj-abbi  32415  eliminable2a  32483  eliminable2b  32484  eliminable2c  32485  bj-df-cleq  32537  bj-sbeq  32540  bj-sbceqgALT  32541  bj-snsetex  32595  bj-df-v  32660  cover2  33137  rp-fakeinunass  37339  intimag  37426  relexp0eq  37471  ntrneik4w  37877  undif3VD  38598  rnmptpr  38829  uzinico  39195  dvnmul  39461  dvnprodlem3  39466  sge00  39897  sge0resplit  39927  sge0fodjrnlem  39937  hspdifhsp  40134  smfresal  40299