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

Theorem dfcleq 2133
Description: The same as df-cleq 2132 with the hypothesis removed using the Axiom of Extensionality ax-ext 2121. (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 2121 . 2  |-  ( A. x ( x  e.  y  <->  x  e.  z
)  ->  y  =  z )
21df-cleq 2132 1  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 104   A.wal 1329    = wceq 1331    e. wcel 1480
This theorem was proved from axioms:  ax-ext 2121
This theorem depends on definitions:  df-cleq 2132
This theorem is referenced by:  cvjust  2134  eqriv  2136  eqrdv  2137  eqcom  2141  eqeq1  2146  eleq2  2203  cleqh  2239  abbi  2253  nfeq  2289  nfeqd  2296  cleqf  2305  eqss  3112  ddifstab  3208  ssequn1  3246  eqv  3382  disj3  3415  undif4  3425  vnex  4059  inex1  4062  zfpair2  4132  sucel  4332  uniex2  4358  bj-vprc  13108  bdinex1  13111  bj-zfpair2  13122  bj-uniex2  13128
  Copyright terms: Public domain W3C validator