New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  eqrdv Unicode version

Theorem eqrdv 2351
 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 1631 . 2
3 dfcleq 2347 . 2
42, 3sylibr 203 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 176  wal 1540   wceq 1642   wcel 1710 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-ext 2334 This theorem depends on definitions:  df-bi 177  df-cleq 2346 This theorem is referenced by:  eqrdav  2352  csbcomg  3159  csbabg  3197  uneq1  3411  ineq1  3450  unineq  3505  difin2  3516  difsn  3845  intmin4  3955  iunconst  3977  iinconst  3978  dfiun2g  3999  iindif2  4035  iinin2  4036  iinxprg  4043  iunxsng  4044  xpkeq1  4198  xpkeq2  4199  eqpw1uni  4330  iotaeq  4347  nnsucelrlem2  4425  dfco2a  5081  imadif  5171  fun11iun  5305  unpreima  5408  inpreima  5409  respreima  5410  fconstfv  5456  funiunfv  5467  erdmrn  5965  enprmaplem5  6080  ncdisjun  6136  nmembers1lem3  6270
 Copyright terms: Public domain W3C validator