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  2957  ssequn1  3110  eqv  3237  disj3  3269  undif4  3281  vprc  3885  inex1  3888  zfpair2  3942  sucel  4143  uniex2  4169  bj-vprc  9889  bdinex1  9892  bj-zfpair2  9903  bj-uniex2  9909
  Copyright terms: Public domain W3C validator