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

Theorem dfcleq 1889
 Description: The same as df-cleq 1888 with the hypothesis removed using the Axiom of Extensionality ax-ext 1877.
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 1877 . 2
21df-cleq 1888 1
 Colors of variables: wff set class Syntax hints:   wb 173  wal 1322   wceq 1398   wcel 1400 This theorem is referenced by:  cvjust  1890  eqriv  1892  eqrdv  1893  eqcom  1897  eqeq1  1901  eleq2  1955  cleqf  1981  hbeq  1991  necompl  2688  eqv  2742  disj3  2760  undif4  2766  sneqbg  2852  dfss2  2879  eqss  2902  ssequn1  2990  axprimlem1  3190  axprimlem2  3191  ninexg  3199  snex  3213  1cex  3246  pw111  3274  opkelimagekg  3375  xpkvexg  3389  p6exg  3394  dfaddc2  3489  nnsucelrlem1  3531  ltfinex  3572  eqtfinrelk  3594  evenfinex  3611  oddfinex  3612  evenodddisjlem1  3623  nnadjoinlem1  3627  dfop2lem1  3681  eqop  3717  setconslem2  3830  dfswap2  3839  brimage  5013  releqel  5028  releqmpt2  5032  qsexg  5194  eq0cprim  5501  elsucprim  5502  eqsucprim  5503  elphiprim  5505  elopprim  5506 This theorem was proved from axioms:  ax-ext 1877 This theorem depends on definitions:  df-cleq 1888
 Copyright terms: Public domain W3C validator