Theorem eqrdv 2229

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 1922	. 2 |- ( ph -> A. x ( x e. A <-> x e. B ) )
3		dfcleq 2225	. 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 2202

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 2213

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

This theorem is referenced by:  eqrdav  2230  eqabdv  2361  csbcomg  3151  csbabg  3190  uneq1  3356  ineq1  3403  difin2  3471  difsn  3815  intmin4  3961  iunconstm  3983  iinconstm  3984  dfiun2g  4007  iindif2m  4043  iinin2m  4044  iunxsng  4051  iunxsngf  4053  iunpw  4583  opthprc  4783  inimasn  5161  dmsnopg  5215  dfco2a  5244  iotaeq  5302  fun11iun  5613  ssimaex  5716  unpreima  5780  respreima  5783  fconstfvm  5880  reldm  6358  suppimacnvfn  6424  suppcofn  6444  rntpos  6466  frecsuclem  6615  iserd  6771  erth  6791  ecidg  6811  mapdm0  6875  map0e  6898  ixpiinm  6936  pw2f1odclem  7063  fifo  7222  ordiso2  7277  ctssdccl  7353  ctssdc  7355  finacn  7462  pw1if  7486  exmidapne  7522  acnccim  7534  genpassl  7787  genpassu  7788  1idprl  7853  1idpru  7854  sup3exmid  9179  eqreznegel  9892  iccid  10204  fzsplit2  10330  fzsn  10346  fzpr  10357  uzsplit  10372  fzoval  10428  infssuzex  10539  frec2uzrand  10713  bitsmod  12580  bitscmp  12582  divsfval  13474  mhmpropd  13612  eqgid  13876  ghmmhmb  13904  ghmpropd  13933  ablnsg  13984  opprsubgg  14161  opprunitd  14188  unitpropdg  14226  opprsubrngg  14289  subsubrng2  14293  subrngpropd  14294  subsubrg2  14324  subrgpropd  14331  rhmpropd  14332  lssats2  14493  lsspropdg  14510  discld  14930  restsn  14974  restdis  14978  cndis  15035  cnpdis  15036  tx1cn  15063  tx2cn  15064  blpnf  15194  blininf  15218  blres  15228  xmetec  15231  metrest  15300  xmetxpbl  15302  cnbl0  15328  reopnap  15340  bl2ioo  15344  cncfmet  15386  limcdifap  15456  gausslemma2dlem1a  15860  ushgredgedg  16150  ushgredgedgloop  16152  clwwlknun  16365  eupth2lemsfi  16402