Theorem dfcleq 2742

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

Syntax hints:   ↔ wb 196  ∀wal 1618   = wceq 1620   ∈ wcel 2127

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-ext 2728

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1842  df-cleq 2741

This theorem is referenced by:  cvjust  2743  eqriv  2745  eqrdv  2746  eqeq1d  2750  eqeq1dALT  2751  eleq2d  2813  eleq2dALT  2814  cleqh  2850  nfeqd  2898  eqss  3747  ssequn1  3914  disj3  4152  undif4  4167  vprc  4936  inex1  4939  axpr  5042  zfpair2  5044  sucel  5947  uniex2  7105  brtxpsd3  32280  hfext  32567  onsuct0  32717  bj-abbi  33052  eliminable2a  33118  eliminable2b  33119  eliminable2c  33120  bj-df-cleq  33170  bj-sbeq  33173  bj-sbceqgALT  33174  bj-snsetex  33228  bj-df-v  33293  cover2  33790  releccnveq  34315  rp-fakeinunass  38332  intimag  38419  relexp0eq  38464  ntrneik4w  38869  undif3VD  39586  rnmptpr  39826  uzinico  40259  dvnmul  40630  dvnprodlem3  40635  sge00  41065  sge0resplit  41095  sge0fodjrnlem  41105  hspdifhsp  41305  smfresal  41470