ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  dfcleq Unicode 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  |-  ( 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 2067 . 2  |-  ( A. x ( x  e.  y  <->  x  e.  z
)  ->  y  =  z )
21df-cleq 2078 1  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 103   A.wal 1285    = wceq 1287    e. 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  3943  inex1  3946  zfpair2  4009  sucel  4209  uniex2  4235  bj-vprc  11216  bdinex1  11219  bj-zfpair2  11230  bj-uniex2  11236
  Copyright terms: Public domain W3C validator