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

Theorem dfcleq 2134
 Description: The same as df-cleq 2133 with the hypothesis removed using the Axiom of Extensionality ax-ext 2122. (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 2122 . 2 (∀𝑥(𝑥𝑦𝑥𝑧) → 𝑦 = 𝑧)
21df-cleq 2133 1 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
 Colors of variables: wff set class Syntax hints:   ↔ wb 104  ∀wal 1330   = wceq 1332   ∈ wcel 1481 This theorem was proved from axioms:  ax-ext 2122 This theorem depends on definitions:  df-cleq 2133 This theorem is referenced by:  cvjust  2135  eqriv  2137  eqrdv  2138  eqcom  2142  eqeq1  2147  eleq2  2204  cleqh  2240  abbi  2254  nfeq  2290  nfeqd  2297  cleqf  2306  eqss  3116  ddifstab  3212  ssequn1  3250  eqv  3386  disj3  3419  undif4  3429  vnex  4066  inex1  4069  zfpair2  4139  sucel  4339  uniex2  4365  bj-vprc  13263  bdinex1  13266  bj-zfpair2  13277  bj-uniex2  13283
 Copyright terms: Public domain W3C validator