Theorem dfcleq 2499

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

Syntax hints:   ↔ wb 191  ∀wal 1466   = wceq 1468   ∈ wcel 1937

This theorem was proved from axioms:  ax-ext 2485

This theorem depends on definitions:  df-cleq 2498

This theorem is referenced by:  cvjust  2500  eqriv  2502  eqrdv  2503  eqeq1d  2507  eqeq1dALT  2508  eleq2d  2568  eleq2dOLD  2569  eleq2dALT  2570  cleqh  2606  nfeqd  2653  eqss  3469  ssequn1  3631  eqv  3774  disj3  3849  undif4  3861  vprc  4574  inex1  4577  axpr  4679  zfpair2  4681  sucel  5547  uniex2  6662  nbcusgra  25352  cusgrauvtxb  25385  bnj145OLD  29688  brtxpsd3  30814  hfext  31101  onsuct0  31250  bj-abbi  31572  eliminable2a  31633  eliminable2b  31634  eliminable2c  31635  bj-ax9  31682  bj-df-cleq  31684  bj-sbeq  31687  bj-sbceqgALT  31688  bj-snsetex  31743  bj-df-v  31806  cover2  32278  rp-fakeinunass  36400  intimag  36487  relexp0eq  36532  undif3VD  37627  dfcleqf  37772  rnmptpr  37805  dvnmul  38237  dvnprodlem3  38242  sge00  38664  sge0resplit  38694  sge0fodjrnlem  38704  hspdifhsp  38901