Theorem eqrdv 2111

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 1826	. 2 |- ( ph -> A. x ( x e. A <-> x e. B ) )
3		dfcleq 2107	. 2 |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
4	2, 3	sylibr 133	1 |- ( ph -> A = B )

Syntax hints:   -> wi 4   <-> wb 104   A.wal 1310   = wceq 1312   e. wcel 1461

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-gen 1406  ax-17 1487  ax-ext 2095

This theorem depends on definitions:  df-bi 116  df-cleq 2106

This theorem is referenced by:  eqrdav  2112  csbcomg  2990  csbabg  3025  uneq1  3187  ineq1  3234  difin2  3302  difsn  3621  intmin4  3763  iunconstm  3785  iinconstm  3786  dfiun2g  3809  iindif2m  3844  iinin2m  3845  iunxsng  3852  iunxsngf  3854  iunpw  4359  opthprc  4548  inimasn  4912  dmsnopg  4966  dfco2a  4995  iotaeq  5052  fun11iun  5342  ssimaex  5434  unpreima  5497  respreima  5500  fconstfvm  5590  reldm  6036  rntpos  6106  frecsuclem  6255  iserd  6407  erth  6425  ecidg  6445  mapdm0  6509  map0e  6532  ixpiinm  6570  fifo  6818  ordiso2  6870  ctssdccl  6946  ctssdc  6948  genpassl  7274  genpassu  7275  1idprl  7340  1idpru  7341  sup3exmid  8619  eqreznegel  9302  iccid  9595  fzsplit2  9717  fzsn  9733  fzpr  9744  uzsplit  9759  fzoval  9812  frec2uzrand  10065  infssuzex  11484  discld  12142  restsn  12186  restdis  12190  cndis  12246  cnpdis  12247  tx1cn  12274  tx2cn  12275  blpnf  12383  blininf  12407  blres  12417  xmetec  12420  metrest  12489  xmetxpbl  12491  cnbl0  12517  bl2ioo  12522  cncfmet  12559  limcdifap  12581