ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  dfcleq Unicode 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  |-  ( 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 2038 . 2  |-  ( A. x ( x  e.  y  <->  x  e.  z
)  ->  y  =  z )
21df-cleq 2049 1  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 102   A.wal 1257    = wceq 1259    e. 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  2988  ssequn1  3141  eqv  3268  disj3  3300  undif4  3312  vprc  3916  inex1  3919  zfpair2  3973  sucel  4175  uniex2  4201  bj-vprc  10403  bdinex1  10406  bj-zfpair2  10417  bj-uniex2  10423
  Copyright terms: Public domain W3C validator