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

Theorem dfcleq 2031
Description: The same as df-cleq 2030 with the hypothesis removed using the Axiom of Extensionality ax-ext 2019. (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 2019 . 2 (x(x yx z) → y = z)
21df-cleq 2030 1 (A = Bx(x Ax B))
Colors of variables: wff set class
Syntax hints:  wb 98  wal 1240   = wceq 1242   wcel 1390
This theorem was proved from axioms:  ax-ext 2019
This theorem depends on definitions:  df-cleq 2030
This theorem is referenced by:  cvjust  2032  eqriv  2034  eqrdv  2035  eqcom  2039  eqeq1  2043  eleq2  2098  cleqh  2134  abbi  2148  nfeq  2182  nfeqd  2189  cleqf  2198  eqss  2954  ssequn1  3107  eqv  3234  disj3  3266  undif4  3278  vprc  3879  inex1  3882  zfpair2  3936  sucel  4113  uniex2  4139  bj-vprc  9327  bdinex1  9330  bj-zfpair2  9341  bj-uniex2  9347
  Copyright terms: Public domain W3C validator