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  5871  reldm  6348  rntpos  6422  frecsuclem  6571  iserd  6727  erth  6747  ecidg  6767  mapdm0  6831  map0e  6854  ixpiinm  6892  pw2f1odclem  7019  fifo  7178  ordiso2  7233  ctssdccl  7309  ctssdc  7311  finacn  7418  pw1if  7442  exmidapne  7478  acnccim  7490  genpassl  7743  genpassu  7744  1idprl  7809  1idpru  7810  sup3exmid  9136  eqreznegel  9847  iccid  10159  fzsplit2  10284  fzsn  10300  fzpr  10311  uzsplit  10326  fzoval  10382  infssuzex  10492  frec2uzrand  10666  bitsmod  12516  bitscmp  12518  divsfval  13410  mhmpropd  13548  eqgid  13812  ghmmhmb  13840  ghmpropd  13869  ablnsg  13920  opprsubgg  14096  opprunitd  14123  unitpropdg  14161  opprsubrngg  14224  subsubrng2  14228  subrngpropd  14229  subsubrg2  14259  subrgpropd  14266  rhmpropd  14267  lssats2  14427  lsspropdg  14444  discld  14859  restsn  14903  restdis  14907  cndis  14964  cnpdis  14965  tx1cn  14992  tx2cn  14993  blpnf  15123  blininf  15147  blres  15157  xmetec  15160  metrest  15229  xmetxpbl  15231  cnbl0  15257  reopnap  15269  bl2ioo  15273  cncfmet  15315  limcdifap  15385  gausslemma2dlem1a  15786  ushgredgedg  16076  ushgredgedgloop  16078  clwwlknun  16291