Theorem eqrdv 2230

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 2226	. 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 2203

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 2214

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

This theorem is referenced by:  eqrdav  2231  abbi  2351  eqabdv  2363  csbcomg  3161  csbabg  3200  uneq1  3366  ineq1  3415  difin2  3483  difsn  3831  intmin4  3977  iunconstm  3999  iinconstm  4000  dfiun2g  4023  iindif2m  4059  iinin2m  4060  iunxsng  4067  iunxsngf  4069  iunpw  4601  opthprc  4801  inimasn  5180  dmsnopg  5234  dfco2a  5263  iotaeq  5321  fun11iun  5635  ssimaex  5738  unpreima  5802  respreima  5805  fconstfvm  5902  reldm  6380  suppimacnvfn  6446  suppcofn  6466  rntpos  6488  frecsuclem  6637  iserd  6793  erth  6813  ecidg  6833  mapdm0  6897  map0e  6920  ixpiinm  6959  pw2f1odclem  7087  fifo  7267  ordiso2  7326  ctssdccl  7402  ctssdc  7404  finacn  7511  pw1if  7535  exmidapne  7574  acnccim  7586  genpassl  7839  genpassu  7840  1idprl  7905  1idpru  7906  sup3exmid  9231  eqreznegel  9946  iccid  10258  fzsplit2  10384  fzsn  10400  fzpr  10411  uzsplit  10426  fzoval  10482  infssuzex  10593  frec2uzrand  10767  bitsmod  12642  bitscmp  12644  divsfval  13541  mhmpropd  13679  eqgid  13943  ghmmhmb  13971  ghmpropd  14000  ablnsg  14051  opprsubgg  14228  opprunitd  14255  unitpropdg  14293  opprsubrngg  14356  subsubrng2  14360  subrngpropd  14361  subsubrg2  14391  subrgpropd  14398  rhmpropd  14399  lssats2  14562  lsspropdg  14579  discld  15001  restsn  15045  restdis  15049  cndis  15106  cnpdis  15107  tx1cn  15134  tx2cn  15135  blpnf  15265  blininf  15289  blres  15299  xmetec  15302  metrest  15371  xmetxpbl  15373  cnbl0  15399  reopnap  15411  bl2ioo  15415  cncfmet  15457  limcdifap  15527  gausslemma2dlem1a  15931  ushgredgedg  16221  ushgredgedgloop  16223  clwwlknun  16436  eupth2lemsfi  16473