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  5593  ssimaex  5695  unpreima  5760  respreima  5763  fconstfvm  5857  reldm  6332  rntpos  6403  frecsuclem  6552  iserd  6706  erth  6726  ecidg  6746  mapdm0  6810  map0e  6833  ixpiinm  6871  pw2f1odclem  6995  fifo  7147  ordiso2  7202  ctssdccl  7278  ctssdc  7280  finacn  7386  pw1if  7410  exmidapne  7446  acnccim  7458  genpassl  7711  genpassu  7712  1idprl  7777  1idpru  7778  sup3exmid  9104  eqreznegel  9809  iccid  10121  fzsplit2  10246  fzsn  10262  fzpr  10273  uzsplit  10288  fzoval  10344  infssuzex  10453  frec2uzrand  10627  bitsmod  12467  bitscmp  12469  divsfval  13361  mhmpropd  13499  eqgid  13763  ghmmhmb  13791  ghmpropd  13820  ablnsg  13871  opprsubgg  14047  opprunitd  14074  unitpropdg  14112  opprsubrngg  14175  subsubrng2  14179  subrngpropd  14180  subsubrg2  14210  subrgpropd  14217  rhmpropd  14218  lssats2  14378  lsspropdg  14395  discld  14810  restsn  14854  restdis  14858  cndis  14915  cnpdis  14916  tx1cn  14943  tx2cn  14944  blpnf  15074  blininf  15098  blres  15108  xmetec  15111  metrest  15180  xmetxpbl  15182  cnbl0  15208  reopnap  15220  bl2ioo  15224  cncfmet  15266  limcdifap  15336  gausslemma2dlem1a  15737  ushgredgedg  16024  ushgredgedgloop  16026