Theorem eqrdv 2175

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

Step	Hyp	Ref	Expression
1		eqrdv.1	. . 3 |- ( ph -> ( x e. A <-> x e. B ) )
2	1	alrimiv 1874	. 2 |- ( ph -> A. x ( x e. A <-> x e. B ) )
3		dfcleq 2171	. 2 |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
4	2, 3	sylibr 134	1 |- ( ph -> A = B )

Syntax hints:   -> wi 4   <-> wb 105   A.wal 1351   = wceq 1353   e. wcel 2148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-17 1526  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170

This theorem is referenced by:  eqrdav  2176  csbcomg  3080  csbabg  3118  uneq1  3282  ineq1  3329  difin2  3397  difsn  3729  intmin4  3872  iunconstm  3894  iinconstm  3895  dfiun2g  3918  iindif2m  3953  iinin2m  3954  iunxsng  3961  iunxsngf  3963  iunpw  4479  opthprc  4676  inimasn  5045  dmsnopg  5099  dfco2a  5128  iotaeq  5185  fun11iun  5481  ssimaex  5576  unpreima  5640  respreima  5643  fconstfvm  5733  reldm  6184  rntpos  6255  frecsuclem  6404  iserd  6558  erth  6576  ecidg  6596  mapdm0  6660  map0e  6683  ixpiinm  6721  fifo  6976  ordiso2  7031  ctssdccl  7107  ctssdc  7109  exmidapne  7256  genpassl  7520  genpassu  7521  1idprl  7586  1idpru  7587  sup3exmid  8910  eqreznegel  9610  iccid  9921  fzsplit2  10045  fzsn  10061  fzpr  10072  uzsplit  10087  fzoval  10143  frec2uzrand  10400  infssuzex  11942  mhmpropd  12789  eqgid  13016  opprunitd  13210  unitpropdg  13248  subsubrg2  13305  subrgpropd  13307  discld  13507  restsn  13551  restdis  13555  cndis  13612  cnpdis  13613  tx1cn  13640  tx2cn  13641  blpnf  13771  blininf  13795  blres  13805  xmetec  13808  metrest  13877  xmetxpbl  13879  cnbl0  13905  reopnap  13909  bl2ioo  13913  cncfmet  13950  limcdifap  14002