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

Theorem dfcleq 2111
Description: The same as df-cleq 2110 with the hypothesis removed using the Axiom of Extensionality ax-ext 2099. (Contributed by NM, 15-Sep-1993.)
Assertion
Ref Expression
dfcleq  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
Distinct variable groups:    x, A    x, B

Proof of Theorem dfcleq
Dummy variables  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ax-ext 2099 . 2  |-  ( A. x ( x  e.  y  <->  x  e.  z
)  ->  y  =  z )
21df-cleq 2110 1  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 104   A.wal 1314    = wceq 1316    e. wcel 1465
This theorem was proved from axioms:  ax-ext 2099
This theorem depends on definitions:  df-cleq 2110
This theorem is referenced by:  cvjust  2112  eqriv  2114  eqrdv  2115  eqcom  2119  eqeq1  2124  eleq2  2181  cleqh  2217  abbi  2231  nfeq  2266  nfeqd  2273  cleqf  2282  eqss  3082  ddifstab  3178  ssequn1  3216  eqv  3352  disj3  3385  undif4  3395  vnex  4029  inex1  4032  zfpair2  4102  sucel  4302  uniex2  4328  bj-vprc  13021  bdinex1  13024  bj-zfpair2  13035  bj-uniex2  13041
  Copyright terms: Public domain W3C validator