ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  dfcleq Structured version   Unicode version

Theorem dfcleq 2016
Description: The same as df-cleq 2015 with the hypothesis removed using the Axiom of Extensionality ax-ext 2004. (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 2004 . 2
21df-cleq 2015 1
Colors of variables: wff set class
Syntax hints:   wb 98  wal 1226   wceq 1228   wcel 1374
This theorem was proved from axioms:  ax-ext 2004
This theorem depends on definitions:  df-cleq 2015
This theorem is referenced by:  cvjust  2017  eqriv  2019  eqrdv  2020  eqcom  2024  eqeq1  2028  eleq2  2083  cleqh  2119  abbi  2133  nfeq  2167  nfeqd  2174  cleqf  2183  eqss  2935  ssequn1  3088  eqv  3215  disj3  3247  undif4  3259  vprc  3860  inex1  3863  zfpair2  3917  sucel  4094  uniex2  4121  bj-vprc  6798  bdinex1  6801  bj-zfpair2  6812  bj-uniex2  6818
  Copyright terms: Public domain W3C validator