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  7239  ordiso2  7294  ctssdccl  7370  ctssdc  7372  finacn  7479  pw1if  7503  exmidapne  7539  acnccim  7551  genpassl  7804  genpassu  7805  1idprl  7870  1idpru  7871  sup3exmid  9196  eqreznegel  9909  iccid  10221  fzsplit2  10347  fzsn  10363  fzpr  10374  uzsplit  10389  fzoval  10445  infssuzex  10556  frec2uzrand  10730  bitsmod  12597  bitscmp  12599  divsfval  13491  mhmpropd  13629  eqgid  13893  ghmmhmb  13921  ghmpropd  13950  ablnsg  14001  opprsubgg  14178  opprunitd  14205  unitpropdg  14243  opprsubrngg  14306  subsubrng2  14310  subrngpropd  14311  subsubrg2  14341  subrgpropd  14348  rhmpropd  14349  lssats2  14510  lsspropdg  14527  discld  14947  restsn  14991  restdis  14995  cndis  15052  cnpdis  15053  tx1cn  15080  tx2cn  15081  blpnf  15211  blininf  15235  blres  15245  xmetec  15248  metrest  15317  xmetxpbl  15319  cnbl0  15345  reopnap  15357  bl2ioo  15361  cncfmet  15403  limcdifap  15473  gausslemma2dlem1a  15877  ushgredgedg  16167  ushgredgedgloop  16169  clwwlknun  16382  eupth2lemsfi  16419