Theorem eqrdv 2227

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 1920	. 2 |- ( ph -> A. x ( x e. A <-> x e. B ) )
3		dfcleq 2223	. 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 1393   = wceq 1395   e. wcel 2200

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 1493  ax-gen 1495  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  eqrdav  2228  eqabdv  2358  csbcomg  3147  csbabg  3186  uneq1  3351  ineq1  3398  difin2  3466  difsn  3805  intmin4  3951  iunconstm  3973  iinconstm  3974  dfiun2g  3997  iindif2m  4033  iinin2m  4034  iunxsng  4041  iunxsngf  4043  iunpw  4571  opthprc  4770  inimasn  5146  dmsnopg  5200  dfco2a  5229  iotaeq  5287  fun11iun  5595  ssimaex  5697  unpreima  5762  respreima  5765  fconstfvm  5861  reldm  6338  rntpos  6409  frecsuclem  6558  iserd  6714  erth  6734  ecidg  6754  mapdm0  6818  map0e  6841  ixpiinm  6879  pw2f1odclem  7003  fifo  7158  ordiso2  7213  ctssdccl  7289  ctssdc  7291  finacn  7397  pw1if  7421  exmidapne  7457  acnccim  7469  genpassl  7722  genpassu  7723  1idprl  7788  1idpru  7789  sup3exmid  9115  eqreznegel  9821  iccid  10133  fzsplit2  10258  fzsn  10274  fzpr  10285  uzsplit  10300  fzoval  10356  infssuzex  10465  frec2uzrand  10639  bitsmod  12483  bitscmp  12485  divsfval  13377  mhmpropd  13515  eqgid  13779  ghmmhmb  13807  ghmpropd  13836  ablnsg  13887  opprsubgg  14063  opprunitd  14090  unitpropdg  14128  opprsubrngg  14191  subsubrng2  14195  subrngpropd  14196  subsubrg2  14226  subrgpropd  14233  rhmpropd  14234  lssats2  14394  lsspropdg  14411  discld  14826  restsn  14870  restdis  14874  cndis  14931  cnpdis  14932  tx1cn  14959  tx2cn  14960  blpnf  15090  blininf  15114  blres  15124  xmetec  15127  metrest  15196  xmetxpbl  15198  cnbl0  15224  reopnap  15236  bl2ioo  15240  cncfmet  15282  limcdifap  15352  gausslemma2dlem1a  15753  ushgredgedg  16040  ushgredgedgloop  16042