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

Theorem dfcleq 2010
Description: The same as df-cleq 2009 with the hypothesis removed using the Axiom of Extensionality ax-ext 1998. (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 1998 . 2
21df-cleq 2009 1
Colors of variables: wff set class
Syntax hints:   wb 98  wal 1224   wceq 1226   wcel 1369
This theorem was proved from axioms:  ax-ext 1998
This theorem depends on definitions:  df-cleq 2009
This theorem is referenced by:  cvjust  2011  eqriv  2013  eqrdv  2014  eqcom  2018  eqeq1  2022  eleq2  2077  cleqh  2113  abbi  2127  nfeq  2161  nfeqd  2168  cleqf  2177  eqss  2931  ssequn1  3084  eqv  3211  disj3  3243  undif4  3255  vprc  3854  inex1  3857  zfpair2  3911  sucel  4088  uniex2  4114  bj-vprc  8469  bdinex1  8472  bj-zfpair2  8483  bj-uniex2  8489
  Copyright terms: Public domain W3C validator