Theorem eqrdv 2191

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 1885	. 2 |- ( ph -> A. x ( x e. A <-> x e. B ) )
3		dfcleq 2187	. 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 1362   = wceq 1364   e. wcel 2164

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 1458  ax-gen 1460  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  eqrdav  2192  eqabdv  2322  csbcomg  3103  csbabg  3142  uneq1  3306  ineq1  3353  difin2  3421  difsn  3755  intmin4  3898  iunconstm  3920  iinconstm  3921  dfiun2g  3944  iindif2m  3980  iinin2m  3981  iunxsng  3988  iunxsngf  3990  iunpw  4511  opthprc  4710  inimasn  5083  dmsnopg  5137  dfco2a  5166  iotaeq  5223  fun11iun  5521  ssimaex  5618  unpreima  5683  respreima  5686  fconstfvm  5776  reldm  6239  rntpos  6310  frecsuclem  6459  iserd  6613  erth  6633  ecidg  6653  mapdm0  6717  map0e  6740  ixpiinm  6778  pw2f1odclem  6890  fifo  7039  ordiso2  7094  ctssdccl  7170  ctssdc  7172  exmidapne  7320  genpassl  7584  genpassu  7585  1idprl  7650  1idpru  7651  sup3exmid  8976  eqreznegel  9679  iccid  9991  fzsplit2  10116  fzsn  10132  fzpr  10143  uzsplit  10158  fzoval  10214  frec2uzrand  10476  infssuzex  12086  divsfval  12911  mhmpropd  13038  eqgid  13296  ghmmhmb  13324  ghmpropd  13353  ablnsg  13404  opprsubgg  13580  opprunitd  13606  unitpropdg  13644  opprsubrngg  13707  subsubrng2  13711  subrngpropd  13712  subsubrg2  13742  subrgpropd  13749  rhmpropd  13750  lssats2  13910  lsspropdg  13927  discld  14304  restsn  14348  restdis  14352  cndis  14409  cnpdis  14410  tx1cn  14437  tx2cn  14438  blpnf  14568  blininf  14592  blres  14602  xmetec  14605  metrest  14674  xmetxpbl  14676  cnbl0  14702  reopnap  14706  bl2ioo  14710  cncfmet  14747  limcdifap  14816  gausslemma2dlem1a  15174