Theorem eqrdv 2229

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 1922	. 2 |- ( ph -> A. x ( x e. A <-> x e. B ) )
3		dfcleq 2225	. 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 1395   = wceq 1397   e. wcel 2202

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 1495  ax-gen 1497  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  eqrdav  2230  eqabdv  2360  csbcomg  3150  csbabg  3189  uneq1  3354  ineq1  3401  difin2  3469  difsn  3810  intmin4  3956  iunconstm  3978  iinconstm  3979  dfiun2g  4002  iindif2m  4038  iinin2m  4039  iunxsng  4046  iunxsngf  4048  iunpw  4577  opthprc  4777  inimasn  5154  dmsnopg  5208  dfco2a  5237  iotaeq  5295  fun11iun  5604  ssimaex  5707  unpreima  5772  respreima  5775  fconstfvm  5872  reldm  6349  rntpos  6423  frecsuclem  6572  iserd  6728  erth  6748  ecidg  6768  mapdm0  6832  map0e  6855  ixpiinm  6893  pw2f1odclem  7020  fifo  7179  ordiso2  7234  ctssdccl  7310  ctssdc  7312  finacn  7419  pw1if  7443  exmidapne  7479  acnccim  7491  genpassl  7744  genpassu  7745  1idprl  7810  1idpru  7811  sup3exmid  9137  eqreznegel  9848  iccid  10160  fzsplit2  10285  fzsn  10301  fzpr  10312  uzsplit  10327  fzoval  10383  infssuzex  10494  frec2uzrand  10668  bitsmod  12535  bitscmp  12537  divsfval  13429  mhmpropd  13567  eqgid  13831  ghmmhmb  13859  ghmpropd  13888  ablnsg  13939  opprsubgg  14116  opprunitd  14143  unitpropdg  14181  opprsubrngg  14244  subsubrng2  14248  subrngpropd  14249  subsubrg2  14279  subrgpropd  14286  rhmpropd  14287  lssats2  14447  lsspropdg  14464  discld  14879  restsn  14923  restdis  14927  cndis  14984  cnpdis  14985  tx1cn  15012  tx2cn  15013  blpnf  15143  blininf  15167  blres  15177  xmetec  15180  metrest  15249  xmetxpbl  15251  cnbl0  15277  reopnap  15289  bl2ioo  15293  cncfmet  15335  limcdifap  15405  gausslemma2dlem1a  15806  ushgredgedg  16096  ushgredgedgloop  16098  clwwlknun  16311  eupth2lemsfi  16348