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

Theorem dfcleq 2050
 Description: The same as df-cleq 2049 with the hypothesis removed using the Axiom of Extensionality ax-ext 2038. (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 2038 . 2 (∀𝑥(𝑥𝑦𝑥𝑧) → 𝑦 = 𝑧)
21df-cleq 2049 1 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
 Colors of variables: wff set class Syntax hints:   ↔ wb 102  ∀wal 1257   = wceq 1259   ∈ wcel 1409 This theorem was proved from axioms:  ax-ext 2038 This theorem depends on definitions:  df-cleq 2049 This theorem is referenced by:  cvjust  2051  eqriv  2053  eqrdv  2054  eqcom  2058  eqeq1  2062  eleq2  2117  cleqh  2153  abbi  2167  nfeq  2201  nfeqd  2208  cleqf  2217  eqss  2987  ssequn1  3140  eqv  3267  disj3  3299  undif4  3311  vprc  3915  inex1  3918  zfpair2  3972  sucel  4174  uniex2  4200  bj-vprc  10382  bdinex1  10385  bj-zfpair2  10396  bj-uniex2  10402
 Copyright terms: Public domain W3C validator