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

Theorem dfcleq 2017
Description: The same as df-cleq 2016 with the hypothesis removed using the Axiom of Extensionality ax-ext 2005. (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 2005 . 2
21df-cleq 2016 1
Colors of variables: wff set class
Syntax hints:   wb 98  wal 1226   wceq 1228   wcel 1375
This theorem was proved from axioms:  ax-ext 2005
This theorem depends on definitions:  df-cleq 2016
This theorem is referenced by:  cvjust  2018  eqriv  2020  eqrdv  2021  eqcom  2025  eqeq1  2029  eleq2  2084  cleqh  2120  abbi  2134  nfeq  2168  nfeqd  2175  cleqf  2184  eqss  2936  ssequn1  3089  eqv  3216  disj3  3248  undif4  3260  vprc  3861  inex1  3864  zfpair2  3918  sucel  4094  uniex2  4121  bj-vprc  6463  bdinex1  6466  bj-zfpair2  6477  bj-uniex2  6483
  Copyright terms: Public domain W3C validator