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  3104  csbabg  3143  uneq1  3307  ineq1  3354  difin2  3422  difsn  3756  intmin4  3899  iunconstm  3921  iinconstm  3922  dfiun2g  3945  iindif2m  3981  iinin2m  3982  iunxsng  3989  iunxsngf  3991  iunpw  4512  opthprc  4711  inimasn  5084  dmsnopg  5138  dfco2a  5167  iotaeq  5224  fun11iun  5522  ssimaex  5619  unpreima  5684  respreima  5687  fconstfvm  5777  reldm  6241  rntpos  6312  frecsuclem  6461  iserd  6615  erth  6635  ecidg  6655  mapdm0  6719  map0e  6742  ixpiinm  6780  pw2f1odclem  6892  fifo  7041  ordiso2  7096  ctssdccl  7172  ctssdc  7174  exmidapne  7322  genpassl  7586  genpassu  7587  1idprl  7652  1idpru  7653  sup3exmid  8978  eqreznegel  9682  iccid  9994  fzsplit2  10119  fzsn  10135  fzpr  10146  uzsplit  10161  fzoval  10217  frec2uzrand  10479  infssuzex  12089  divsfval  12914  mhmpropd  13041  eqgid  13299  ghmmhmb  13327  ghmpropd  13356  ablnsg  13407  opprsubgg  13583  opprunitd  13609  unitpropdg  13647  opprsubrngg  13710  subsubrng2  13714  subrngpropd  13715  subsubrg2  13745  subrgpropd  13752  rhmpropd  13753  lssats2  13913  lsspropdg  13930  discld  14315  restsn  14359  restdis  14363  cndis  14420  cnpdis  14421  tx1cn  14448  tx2cn  14449  blpnf  14579  blininf  14603  blres  14613  xmetec  14616  metrest  14685  xmetxpbl  14687  cnbl0  14713  reopnap  14725  bl2ioo  14729  cncfmet  14771  limcdifap  14841  gausslemma2dlem1a  15215