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  suppinisegdc  6513  rntpos  6533  frecsuclem  6682  iserd  6838  erth  6858  ecidg  6878  mapdm0  6942  mapfset  6950  map0e  6972  ixpiinm  7012  pw2f1odclem  7140  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  10029  iccid  10343  fzsplit2  10471  fzsplit3  10474  fzsn  10488  fzpr  10500  uzsplit  10515  fzoval  10571  infssuzex  10682  frec2uzrand  10862  bitsmod  12747  bitscmp  12749  divsfval  13707  mhmpropd  13831  eqgid  14087  ghmmhmb  14115  ghmpropd  14144  cntzval  14152  resscntz  14165  ablnsg  14227  idjusnfi  14269  gsum2d2fi  14273  opprsubgg  14498  opprunitd  14525  unitpropdg  14563  opprsubrngg  14627  subsubrng2  14631  subrngpropd  14632  subsubrg2  14662  subrgpropd  14669  rhmpropd  14670  ringunitsap0  14702  drnguiap  14717  lssats2  14859  lsspropdg  14876  discld  15379  restsn  15423  restdis  15427  cndis  15484  cnpdis  15485  tx1cn  15512  tx2cn  15513  blpnf  15643  blininf  15667  blres  15677  xmetec  15680  metrest  15749  xmetxpbl  15751  cnbl0  15777  reopnap  15789  bl2ioo  15793  cncfmet  15835  limcdifap  15905  gausslemma2dlem1a  16399  ushgredgedg  16689  ushgredgedgloop  16691  clwwlknun  16904  eupth2lemsfi  16941