Theorem eqrdv 2203

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 1897	. 2 |- ( ph -> A. x ( x e. A <-> x e. B ) )
3		dfcleq 2199	. 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 1371   = wceq 1373   e. wcel 2176

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 1470  ax-gen 1472  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  eqrdav  2204  eqabdv  2334  csbcomg  3116  csbabg  3155  uneq1  3320  ineq1  3367  difin2  3435  difsn  3770  intmin4  3913  iunconstm  3935  iinconstm  3936  dfiun2g  3959  iindif2m  3995  iinin2m  3996  iunxsng  4003  iunxsngf  4005  iunpw  4528  opthprc  4727  inimasn  5101  dmsnopg  5155  dfco2a  5184  iotaeq  5241  fun11iun  5545  ssimaex  5642  unpreima  5707  respreima  5710  fconstfvm  5804  reldm  6274  rntpos  6345  frecsuclem  6494  iserd  6648  erth  6668  ecidg  6688  mapdm0  6752  map0e  6775  ixpiinm  6813  pw2f1odclem  6933  fifo  7084  ordiso2  7139  ctssdccl  7215  ctssdc  7217  finacn  7318  exmidapne  7374  acnccim  7386  genpassl  7639  genpassu  7640  1idprl  7705  1idpru  7706  sup3exmid  9032  eqreznegel  9737  iccid  10049  fzsplit2  10174  fzsn  10190  fzpr  10201  uzsplit  10216  fzoval  10272  infssuzex  10378  frec2uzrand  10552  bitsmod  12300  bitscmp  12302  divsfval  13193  mhmpropd  13331  eqgid  13595  ghmmhmb  13623  ghmpropd  13652  ablnsg  13703  opprsubgg  13879  opprunitd  13905  unitpropdg  13943  opprsubrngg  14006  subsubrng2  14010  subrngpropd  14011  subsubrg2  14041  subrgpropd  14048  rhmpropd  14049  lssats2  14209  lsspropdg  14226  discld  14641  restsn  14685  restdis  14689  cndis  14746  cnpdis  14747  tx1cn  14774  tx2cn  14775  blpnf  14905  blininf  14929  blres  14939  xmetec  14942  metrest  15011  xmetxpbl  15013  cnbl0  15039  reopnap  15051  bl2ioo  15055  cncfmet  15097  limcdifap  15167  gausslemma2dlem1a  15568