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 )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   A.wal 1400   = wceq 1402   e. wcel 2209

This proof depends on 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 proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  eqrdav  2237  abbi  2357  eqabdv  2369  csbcomg  3170  csbabg  3209  uneq1  3376  ineq1  3425  difin2  3493  difsn  3852  intmin4  3998  iunconstm  4020  iinconstm  4021  dfiun2g  4044  iindif2m  4080  iinin2m  4081  iunxsng  4088  iunxsngf  4090  iunpw  4628  opthprc  4828  inimasn  5208  dmsnopg  5262  dfco2a  5291  iotaeq  5349  fun11iun  5663  relndmfv  5731  ssimaex  5767  unpreima  5836  respreima  5839  fconstfvm  5936  reldm  6424  suppimacnvfn  6490  suppcofn  6510  rntpos  6532  frecsuclem  6681  iserd  6837  erth  6857  ecidg  6877  mapdm0  6941  mapfset  6949  map0e  6971  ixpiinm  7010  pw2f1odclem  7138  fifo  7319  ordiso2  7381  ctssdccl  7457  ctssdc  7459  finacn  7566  pw1if  7590  exmidapne  7632  acnccim  7644  genpassl  7897  genpassu  7898  1idprl  7963  1idpru  7964  sup3exmid  9295  indval0  9306  eqreznegel  10030  iccid  10344  fzsplit2  10472  fzsplit3  10475  fzsn  10489  fzpr  10501  uzsplit  10516  fzoval  10572  infssuzex  10683  frec2uzrand  10863  bitsmod  12748  bitscmp  12750  divsfval  13708  mhmpropd  13832  eqgid  14088  ghmmhmb  14116  ghmpropd  14145  cntzval  14153  resscntz  14166  ablnsg  14228  idjusnfi  14270  gsum2d2fi  14274  opprsubgg  14499  opprunitd  14526  unitpropdg  14564  opprsubrngg  14628  subsubrng2  14632  subrngpropd  14633  subsubrg2  14663  subrgpropd  14670  rhmpropd  14671  ringunitsap0  14703  drnguiap  14718  lssats2  14860  lsspropdg  14877  discld  15362  restsn  15406  restdis  15410  cndis  15467  cnpdis  15468  tx1cn  15495  tx2cn  15496  blpnf  15626  blininf  15650  blres  15660  xmetec  15663  metrest  15732  xmetxpbl  15734  cnbl0  15760  reopnap  15772  bl2ioo  15776  cncfmet  15818  limcdifap  15888  gausslemma2dlem1a  16382  ushgredgedg  16672  ushgredgedgloop  16674  clwwlknun  16887  eupth2lemsfi  16924