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

Theorem eqrdv 2115
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 1830 . 2  |-  ( ph  ->  A. x ( x  e.  A  <->  x  e.  B ) )
3 dfcleq 2111 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
42, 3sylibr 133 1  |-  ( ph  ->  A  =  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104   A.wal 1314    = wceq 1316    e. wcel 1465
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1408  ax-gen 1410  ax-17 1491  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-cleq 2110
This theorem is referenced by:  eqrdav  2116  csbcomg  2996  csbabg  3031  uneq1  3193  ineq1  3240  difin2  3308  difsn  3627  intmin4  3769  iunconstm  3791  iinconstm  3792  dfiun2g  3815  iindif2m  3850  iinin2m  3851  iunxsng  3858  iunxsngf  3860  iunpw  4371  opthprc  4560  inimasn  4926  dmsnopg  4980  dfco2a  5009  iotaeq  5066  fun11iun  5356  ssimaex  5450  unpreima  5513  respreima  5516  fconstfvm  5606  reldm  6052  rntpos  6122  frecsuclem  6271  iserd  6423  erth  6441  ecidg  6461  mapdm0  6525  map0e  6548  ixpiinm  6586  fifo  6836  ordiso2  6888  ctssdccl  6964  ctssdc  6966  genpassl  7300  genpassu  7301  1idprl  7366  1idpru  7367  sup3exmid  8683  eqreznegel  9374  iccid  9676  fzsplit2  9798  fzsn  9814  fzpr  9825  uzsplit  9840  fzoval  9893  frec2uzrand  10146  infssuzex  11569  discld  12232  restsn  12276  restdis  12280  cndis  12337  cnpdis  12338  tx1cn  12365  tx2cn  12366  blpnf  12496  blininf  12520  blres  12530  xmetec  12533  metrest  12602  xmetxpbl  12604  cnbl0  12630  reopnap  12634  bl2ioo  12638  cncfmet  12675  limcdifap  12727
  Copyright terms: Public domain W3C validator