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

Theorem eqrdv 2020
Description: Deduce equality of classes from equivalence of membership. (Contributed by NM, 17-Mar-1996.)
Hypothesis
Ref Expression
eqrdv.1
Assertion
Ref Expression
eqrdv
Distinct variable groups:   ,   ,   ,

Proof of Theorem eqrdv
StepHypRef Expression
1 eqrdv.1 . . 3
21alrimiv 1736 . 2
3 dfcleq 2016 . 2
42, 3sylibr 137 1
Colors of variables: wff set class
Syntax hints:   wi 4   wb 98  wal 1226   wceq 1228   wcel 1374
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1316  ax-gen 1318  ax-17 1400  ax-ext 2004
This theorem depends on definitions:  df-bi 110  df-cleq 2015
This theorem is referenced by:  eqrdav  2021  csbcomg  2850  csbabg  2884  uneq1  3067  ineq1  3108  difin2  3176  difsn  3475  intmin4  3617  iunconstm  3639  iinconstm  3640  dfiun2g  3663  iindif2m  3698  iinin2m  3699  iunxsng  3706  iunpw  4161  opthprc  4318  inimasn  4668  dmsnopg  4719  dfco2a  4748  iotaeq  4802  fun11iun  5072  ssimaex  5159  unpreima  5217  respreima  5220  fconstfvm  5304  reldm  5735  rntpos  5794  frecsuclem3  5906  iserd  6043  erth  6061  ecidg  6081  genpassl  6379  genpassu  6380  1idprl  6429  1idpru  6430
  Copyright terms: Public domain W3C validator