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

Theorem dfcleq 2183
Description: The same as df-cleq 2182 with the hypothesis removed using the Axiom of Extensionality ax-ext 2171. (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 2171 . 2 (∀𝑥(𝑥𝑦𝑥𝑧) → 𝑦 = 𝑧)
21df-cleq 2182 1 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
Colors of variables: wff set class
Syntax hints:  wb 105  wal 1362   = wceq 1364  wcel 2160
This theorem was proved from axioms:  ax-ext 2171
This theorem depends on definitions:  df-cleq 2182
This theorem is referenced by:  cvjust  2184  eqriv  2186  eqrdv  2187  eqcom  2191  eqeq1  2196  eleq2  2253  cleqh  2289  abbi  2303  nfeq  2340  nfeqd  2347  cleqf  2357  eqss  3185  ddifstab  3282  ssequn1  3320  eqv  3457  disj3  3490  undif4  3500  vnex  4149  inex1  4152  zfpair2  4228  sucel  4428  uniex2  4454  bj-vprc  15101  bdinex1  15104  bj-zfpair2  15115  bj-uniex2  15121
  Copyright terms: Public domain W3C validator