NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  dfcleq Unicode version

Theorem dfcleq 2347
Description: The same as df-cleq 2346 with the hypothesis removed using the Axiom of Extensionality ax-ext 2334. (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.
StepHypRef Expression
1 ax-ext 2334 . 2
21df-cleq 2346 1
Colors of variables: wff set class
Syntax hints:   wb 176  wal 1540   wceq 1642   wcel 1710
This theorem is referenced by:  cvjust  2348  eqriv  2350  eqrdv  2351  eqcom  2355  eqeq1  2359  eleq2  2414  cleqh  2450  abbi  2463  nfeq  2496  nfeqd  2503  cleqf  2513  dfss2  3262  eqss  3287  ssequn1  3433  necompl  3544  eqv  3565  disj3  3595  undif4  3607  axprimlem1  4088  axprimlem2  4089  ninexg  4097  1cex  4142  pw111  4170  opkelimagekg  4271  xpkvexg  4285  p6exg  4290  dfaddc2  4381  nnsucelrlem1  4423  ltfinex  4464  eqtfinrelk  4486  evenfinex  4503  oddfinex  4504  evenodddisjlem1  4515  nnadjoinlem1  4519  dfop2lem1  4573  eqop  4609  setconslem2  4724  dfswap2  4733  brimage  5822  releqel  5837  releqmpt2  5841  qsexg  6002
This theorem was proved from axioms:  ax-ext 2334
This theorem depends on definitions:  df-cleq 2346
  Copyright terms: Public domain W3C validator