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

Theorem dfcleq 2020
Description: The same as df-cleq 2019 with the hypothesis removed using the Axiom of Extensionality ax-ext 2008. (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 2008 . 2 (x(x yx z) → y = z)
21df-cleq 2019 1 (A = Bx(x Ax B))
Colors of variables: wff set class
Syntax hints:  wb 98  wal 1231   = wceq 1233   wcel 1380
This theorem was proved from axioms:  ax-ext 2008
This theorem depends on definitions:  df-cleq 2019
This theorem is referenced by:  cvjust  2021  eqriv  2023  eqrdv  2024  eqcom  2028  eqeq1  2032  eleq2  2087  cleqh  2123  abbi  2137  nfeq  2171  nfeqd  2178  cleqf  2187  eqss  2939  ssequn1  3092  eqv  3219  disj3  3251  undif4  3263  vprc  3864  inex1  3867  zfpair2  3921  sucel  4096  uniex2  4123  bdinex1  6374  bj-zfpair2  6380  bj-uniex2  6386
  Copyright terms: Public domain W3C validator