Theorem eqrdv 2205

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 1898	. 2 |- ( ph -> A. x ( x e. A <-> x e. B ) )
3		dfcleq 2201	. 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 2178

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 1471  ax-gen 1473  ax-17 1550  ax-ext 2189

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

This theorem is referenced by:  eqrdav  2206  eqabdv  2336  csbcomg  3124  csbabg  3163  uneq1  3328  ineq1  3375  difin2  3443  difsn  3781  intmin4  3927  iunconstm  3949  iinconstm  3950  dfiun2g  3973  iindif2m  4009  iinin2m  4010  iunxsng  4017  iunxsngf  4019  iunpw  4545  opthprc  4744  inimasn  5119  dmsnopg  5173  dfco2a  5202  iotaeq  5259  fun11iun  5565  ssimaex  5663  unpreima  5728  respreima  5731  fconstfvm  5825  reldm  6295  rntpos  6366  frecsuclem  6515  iserd  6669  erth  6689  ecidg  6709  mapdm0  6773  map0e  6796  ixpiinm  6834  pw2f1odclem  6956  fifo  7108  ordiso2  7163  ctssdccl  7239  ctssdc  7241  finacn  7347  pw1if  7371  exmidapne  7407  acnccim  7419  genpassl  7672  genpassu  7673  1idprl  7738  1idpru  7739  sup3exmid  9065  eqreznegel  9770  iccid  10082  fzsplit2  10207  fzsn  10223  fzpr  10234  uzsplit  10249  fzoval  10305  infssuzex  10413  frec2uzrand  10587  bitsmod  12382  bitscmp  12384  divsfval  13275  mhmpropd  13413  eqgid  13677  ghmmhmb  13705  ghmpropd  13734  ablnsg  13785  opprsubgg  13961  opprunitd  13987  unitpropdg  14025  opprsubrngg  14088  subsubrng2  14092  subrngpropd  14093  subsubrg2  14123  subrgpropd  14130  rhmpropd  14131  lssats2  14291  lsspropdg  14308  discld  14723  restsn  14767  restdis  14771  cndis  14828  cnpdis  14829  tx1cn  14856  tx2cn  14857  blpnf  14987  blininf  15011  blres  15021  xmetec  15024  metrest  15093  xmetxpbl  15095  cnbl0  15121  reopnap  15133  bl2ioo  15137  cncfmet  15179  limcdifap  15249  gausslemma2dlem1a  15650