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

Theorem dfcleq 2034
Description: The same as df-cleq 2033 with the hypothesis removed using the Axiom of Extensionality ax-ext 2022. (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 2022 . 2 (∀𝑥(𝑥𝑦𝑥𝑧) → 𝑦 = 𝑧)
21df-cleq 2033 1 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
Colors of variables: wff set class
Syntax hints:  wb 98  wal 1241   = wceq 1243  wcel 1393
This theorem was proved from axioms:  ax-ext 2022
This theorem depends on definitions:  df-cleq 2033
This theorem is referenced by:  cvjust  2035  eqriv  2037  eqrdv  2038  eqcom  2042  eqeq1  2046  eleq2  2101  cleqh  2137  abbi  2151  nfeq  2185  nfeqd  2192  cleqf  2201  eqss  2960  ssequn1  3113  eqv  3240  disj3  3272  undif4  3284  vprc  3888  inex1  3891  zfpair2  3945  sucel  4147  uniex2  4173  bj-vprc  10016  bdinex1  10019  bj-zfpair2  10030  bj-uniex2  10036
  Copyright terms: Public domain W3C validator