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

Theorem dfcleq 2094
Description: The same as df-cleq 2093 with the hypothesis removed using the Axiom of Extensionality ax-ext 2082. (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 2082 . 2 (∀𝑥(𝑥𝑦𝑥𝑧) → 𝑦 = 𝑧)
21df-cleq 2093 1 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
Colors of variables: wff set class
Syntax hints:  wb 104  wal 1297   = wceq 1299  wcel 1448
This theorem was proved from axioms:  ax-ext 2082
This theorem depends on definitions:  df-cleq 2093
This theorem is referenced by:  cvjust  2095  eqriv  2097  eqrdv  2098  eqcom  2102  eqeq1  2106  eleq2  2163  cleqh  2199  abbi  2213  nfeq  2248  nfeqd  2255  cleqf  2264  eqss  3062  ddifstab  3155  ssequn1  3193  eqv  3329  disj3  3362  undif4  3372  vnex  3999  inex1  4002  zfpair2  4070  sucel  4270  uniex2  4296  bj-vprc  12675  bdinex1  12678  bj-zfpair2  12689  bj-uniex2  12695
  Copyright terms: Public domain W3C validator