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

Theorem dfcleq 2079
Description: The same as df-cleq 2078 with the hypothesis removed using the Axiom of Extensionality ax-ext 2067. (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 2067 . 2 (∀𝑥(𝑥𝑦𝑥𝑧) → 𝑦 = 𝑧)
21df-cleq 2078 1 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
Colors of variables: wff set class
Syntax hints:  wb 103  wal 1285   = wceq 1287  wcel 1436
This theorem was proved from axioms:  ax-ext 2067
This theorem depends on definitions:  df-cleq 2078
This theorem is referenced by:  cvjust  2080  eqriv  2082  eqrdv  2083  eqcom  2087  eqeq1  2091  eleq2  2148  cleqh  2184  abbi  2198  nfeq  2232  nfeqd  2239  cleqf  2248  eqss  3029  ddifstab  3121  ssequn1  3159  eqv  3291  disj3  3323  undif4  3333  vnex  3945  inex1  3948  zfpair2  4011  sucel  4211  uniex2  4237  bj-vprc  11232  bdinex1  11235  bj-zfpair2  11246  bj-uniex2  11252
  Copyright terms: Public domain W3C validator