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

Theorem eqrdv 2054
Description: Deduce equality of classes from equivalence of membership. (Contributed by NM, 17-Mar-1996.)
Hypothesis
Ref Expression
eqrdv.1  |-  ( ph  ->  ( x  e.  A  <->  x  e.  B ) )
Assertion
Ref Expression
eqrdv  |-  ( ph  ->  A  =  B )
Distinct variable groups:    x, A    x, B    ph, x

Proof of Theorem eqrdv
StepHypRef Expression
1 eqrdv.1 . . 3  |-  ( ph  ->  ( x  e.  A  <->  x  e.  B ) )
21alrimiv 1770 . 2  |-  ( ph  ->  A. x ( x  e.  A  <->  x  e.  B ) )
3 dfcleq 2050 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
42, 3sylibr 141 1  |-  ( ph  ->  A  =  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 102   A.wal 1257    = wceq 1259    e. wcel 1409
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-17 1435  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-cleq 2049
This theorem is referenced by:  eqrdav  2055  csbcomg  2900  csbabg  2934  uneq1  3117  ineq1  3158  difin2  3226  difsn  3528  intmin4  3670  iunconstm  3692  iinconstm  3693  dfiun2g  3716  iindif2m  3751  iinin2m  3752  iunxsng  3759  iunpw  4238  opthprc  4418  inimasn  4768  dmsnopg  4819  dfco2a  4848  iotaeq  4902  fun11iun  5174  ssimaex  5261  unpreima  5319  respreima  5322  fconstfvm  5406  reldm  5839  rntpos  5902  frecsuclem3  6020  iserd  6162  erth  6180  ecidg  6200  ordiso2  6414  genpassl  6679  genpassu  6680  1idprl  6745  1idpru  6746  eqreznegel  8645  iccid  8894  fzsplit2  9015  fzsn  9030  fzpr  9040  uzsplit  9055  fzoval  9106  frec2uzrand  9354
  Copyright terms: Public domain W3C validator