ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  dfcleq Structured version   GIF 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 (A = Bx(x Ax B))
Distinct variable groups:   x,A   x,B

Proof of Theorem dfcleq
Dummy variables y z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ax-ext 2004 . 2 (x(x yx z) → y = z)
21df-cleq 2015 1 (A = Bx(x Ax B))
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  2937  ssequn1  3090  eqv  3217  disj3  3249  undif4  3261  vprc  3862  inex1  3865  zfpair2  3919  sucel  4096  uniex2  4123  bj-vprc  7119  bdinex1  7122  bj-zfpair2  7133  bj-uniex2  7139
  Copyright terms: Public domain W3C validator