Theorem dfcleq 2616

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

Assertion

Ref	Expression
dfcleq	|- ( A = B <-> A. x ( x e. A <-> x e. B ) )

Distinct variable groups:   x, A   x, B

Proof of Theorem dfcleq

Dummy variables y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		axext3 2604	. 2 |- ( A. x ( x e. y <-> x e. z ) -> y = z )
2	1	df-cleq 2615	1 |- ( A = B <-> A. x ( x e. A <-> x e. B ) )

Syntax hints:   <-> wb 196   A.wal 1481   = wceq 1483   e. wcel 1990

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615

This theorem is referenced by:  cvjust  2617  eqriv  2619  eqrdv  2620  eqeq1d  2624  eqeq1dALT  2625  eleq2d  2687  eleq2dALT  2688  cleqh  2724  nfeqd  2772  eqss  3618  ssequn1  3783  disj3  4021  undif4  4035  vprc  4796  inex1  4799  axpr  4905  zfpair2  4907  sucel  5798  uniex2  6952  bnj145OLD  30795  brtxpsd3  32003  hfext  32290  onsuct0  32440  bj-abbi  32775  eliminable2a  32841  eliminable2b  32842  eliminable2c  32843  bj-df-cleq  32893  bj-sbeq  32896  bj-sbceqgALT  32897  bj-snsetex  32951  bj-df-v  33016  cover2  33508  releccnveq  34022  rp-fakeinunass  37861  intimag  37948  relexp0eq  37993  ntrneik4w  38398  undif3VD  39118  rnmptpr  39358  uzinico  39787  dvnmul  40158  dvnprodlem3  40163  sge00  40593  sge0resplit  40623  sge0fodjrnlem  40633  hspdifhsp  40830  smfresal  40995