Theorem eqrdv 2236

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 1927	. 2 |- ( ph -> A. x ( x e. A <-> x e. B ) )
3		dfcleq 2232	. 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 1400   = wceq 1402   e. wcel 2209

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 1500  ax-gen 1502  ax-17 1579  ax-ext 2220

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

This theorem is referenced by:  eqrdav  2237  abbi  2357  eqabdv  2369  csbcomg  3170  csbabg  3209  uneq1  3376  ineq1  3425  difin2  3493  difsn  3847  intmin4  3993  iunconstm  4015  iinconstm  4016  dfiun2g  4039  iindif2m  4075  iinin2m  4076  iunxsng  4083  iunxsngf  4085  iunpw  4621  opthprc  4821  inimasn  5200  dmsnopg  5254  dfco2a  5283  iotaeq  5341  fun11iun  5655  ssimaex  5758  unpreima  5824  respreima  5827  fconstfvm  5924  reldm  6410  suppimacnvfn  6476  suppcofn  6496  rntpos  6518  frecsuclem  6667  iserd  6823  erth  6843  ecidg  6863  mapdm0  6927  mapfset  6935  map0e  6957  ixpiinm  6996  pw2f1odclem  7124  fifo  7304  ordiso2  7365  ctssdccl  7441  ctssdc  7443  finacn  7550  pw1if  7574  exmidapne  7616  acnccim  7628  genpassl  7881  genpassu  7882  1idprl  7947  1idpru  7948  sup3exmid  9277  eqreznegel  9993  iccid  10306  fzsplit2  10433  fzsplit3  10436  fzsn  10450  fzpr  10462  uzsplit  10477  fzoval  10533  infssuzex  10644  frec2uzrand  10820  bitsmod  12701  bitscmp  12703  divsfval  13626  mhmpropd  13750  eqgid  14006  ghmmhmb  14034  ghmpropd  14063  ablnsg  14115  opprsubgg  14363  opprunitd  14390  unitpropdg  14428  opprsubrngg  14492  subsubrng2  14496  subrngpropd  14497  subsubrg2  14527  subrgpropd  14534  rhmpropd  14535  ringunitsap0  14567  drnguiap  14582  lssats2  14723  lsspropdg  14740  discld  15160  restsn  15204  restdis  15208  cndis  15265  cnpdis  15266  tx1cn  15293  tx2cn  15294  blpnf  15424  blininf  15448  blres  15458  xmetec  15461  metrest  15530  xmetxpbl  15532  cnbl0  15558  reopnap  15570  bl2ioo  15574  cncfmet  15616  limcdifap  15686  gausslemma2dlem1a  16091  ushgredgedg  16381  ushgredgedgloop  16383  clwwlknun  16596  eupth2lemsfi  16633