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  4626  opthprc  4826  inimasn  5205  dmsnopg  5259  dfco2a  5288  iotaeq  5346  fun11iun  5660  relndmfv  5728  ssimaex  5764  unpreima  5833  respreima  5836  fconstfvm  5933  reldm  6420  suppimacnvfn  6486  suppcofn  6506  rntpos  6528  frecsuclem  6677  iserd  6833  erth  6853  ecidg  6873  mapdm0  6937  mapfset  6945  map0e  6967  ixpiinm  7006  pw2f1odclem  7134  fifo  7314  ordiso2  7375  ctssdccl  7451  ctssdc  7453  finacn  7560  pw1if  7584  exmidapne  7626  acnccim  7638  genpassl  7891  genpassu  7892  1idprl  7957  1idpru  7958  sup3exmid  9289  indval0  9299  eqreznegel  10023  iccid  10337  fzsplit2  10465  fzsplit3  10468  fzsn  10482  fzpr  10494  uzsplit  10509  fzoval  10565  infssuzex  10676  frec2uzrand  10855  bitsmod  12739  bitscmp  12741  divsfval  13698  mhmpropd  13822  eqgid  14078  ghmmhmb  14106  ghmpropd  14135  ablnsg  14187  opprsubgg  14439  opprunitd  14466  unitpropdg  14504  opprsubrngg  14568  subsubrng2  14572  subrngpropd  14573  subsubrg2  14603  subrgpropd  14610  rhmpropd  14611  ringunitsap0  14643  drnguiap  14658  lssats2  14800  lsspropdg  14817  discld  15286  restsn  15330  restdis  15334  cndis  15391  cnpdis  15392  tx1cn  15419  tx2cn  15420  blpnf  15550  blininf  15574  blres  15584  xmetec  15587  metrest  15656  xmetxpbl  15658  cnbl0  15684  reopnap  15696  bl2ioo  15700  cncfmet  15742  limcdifap  15812  gausslemma2dlem1a  16275  ushgredgedg  16565  ushgredgedgloop  16567  clwwlknun  16780  eupth2lemsfi  16817