Theorem dfcleq 2450

Description: The same as df-cleq 2449 with the hypothesis removed using the Axiom of Extensionality ax-ext 2435. (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 2435	. 2
2	1	df-cleq 2449	1

Syntax hints:  <->wb 184  A.wal 1393  =wceq 1395  e.wcel 1818

This theorem is referenced by:  cvjust  2451  eqriv  2453  eqrdv  2454  eqeq1d  2459  eqeq1dALT  2460  eqeq1OLD  2462  eqcomOLD  2467  eleq2d  2527  eleq2dALT  2528  eleq2OLD  2532  cleqh  2572  cleqhOLD  2573  abbiOLD  2589  nfeqd  2626  nfeqOLD  2631  cleqfOLD  2647  eqss  3518  ssequn1  3673  eqv  3801  disj3  3871  undif4  3883  vprc  4590  inex1  4593  axpr  4690  zfpair2  4692  sucel  4956  uniex2  6595  nbcusgra  24463  cusgrauvtxb  24496  brtxpsd3  29546  hfext  29840  onsuct0  29906  cover2  30204  dvnmul  31740  dvnprodlem3  31745  undif3VD  33682  bnj145OLD  33782  bj-cleqh  34358  bj-abbi  34361  eliminable2a  34416  eliminable2b  34417  eliminable2c  34418  bj-ax9  34464  bj-df-cleq  34465  bj-sbeq  34468  bj-sbceqgALT  34469  bj-snsetex  34521  bj-df-v  34583  rp-fakeinunass  37740  intimag  37770

This theorem was proved from axioms:  ax-ext 2435

This theorem depends on definitions:  df-cleq 2449