Theorem eqrdv 2232

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 1923	. 2 |- ( ph -> A. x ( x e. A <-> x e. B ) )
3		dfcleq 2228	. 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 1396   = wceq 1398   e. wcel 2205

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 1496  ax-gen 1498  ax-17 1575  ax-ext 2216

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

This theorem is referenced by:  eqrdav  2233  abbi  2353  eqabdv  2365  csbcomg  3164  csbabg  3203  uneq1  3370  ineq1  3419  difin2  3487  difsn  3836  intmin4  3982  iunconstm  4004  iinconstm  4005  dfiun2g  4028  iindif2m  4064  iinin2m  4065  iunxsng  4072  iunxsngf  4074  iunpw  4606  opthprc  4806  inimasn  5185  dmsnopg  5239  dfco2a  5268  iotaeq  5326  fun11iun  5640  ssimaex  5743  unpreima  5807  respreima  5810  fconstfvm  5907  reldm  6393  suppimacnvfn  6459  suppcofn  6479  rntpos  6501  frecsuclem  6650  iserd  6806  erth  6826  ecidg  6846  mapdm0  6910  map0e  6933  ixpiinm  6972  pw2f1odclem  7100  fifo  7280  ordiso2  7339  ctssdccl  7415  ctssdc  7417  finacn  7524  pw1if  7548  exmidapne  7590  acnccim  7602  genpassl  7855  genpassu  7856  1idprl  7921  1idpru  7922  sup3exmid  9248  eqreznegel  9964  iccid  10277  fzsplit2  10404  fzsplit3  10407  fzsn  10421  fzpr  10433  uzsplit  10448  fzoval  10504  infssuzex  10615  frec2uzrand  10791  bitsmod  12667  bitscmp  12669  divsfval  13592  mhmpropd  13721  eqgid  13979  ghmmhmb  14007  ghmpropd  14036  ablnsg  14087  opprsubgg  14328  opprunitd  14355  unitpropdg  14393  opprsubrngg  14457  subsubrng2  14461  subrngpropd  14462  subsubrg2  14492  subrgpropd  14499  rhmpropd  14500  ringunitsap0  14532  drnguiap  14547  lssats2  14688  lsspropdg  14705  discld  15127  restsn  15171  restdis  15175  cndis  15232  cnpdis  15233  tx1cn  15260  tx2cn  15261  blpnf  15391  blininf  15415  blres  15425  xmetec  15428  metrest  15497  xmetxpbl  15499  cnbl0  15525  reopnap  15537  bl2ioo  15541  cncfmet  15583  limcdifap  15653  gausslemma2dlem1a  16057  ushgredgedg  16347  ushgredgedgloop  16349  clwwlknun  16562  eupth2lemsfi  16599