Theorem eqrdv 2732

Description: Deduce equality of classes from equivalence of membership. (Contributed by NM, 17-Mar-1996.)

Hypothesis

Ref	Expression
eqrdv.1	⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))

Assertion

Ref	Expression
eqrdv	⊢ (𝜑 → 𝐴 = 𝐵)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜑,𝑥

Proof of Theorem eqrdv

Step	Hyp	Ref	Expression
1		eqrdv.1	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	alrimiv 1924	. 2 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3		dfcleq 2727	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4	2, 3	sylibr 234	1 ⊢ (𝜑 → 𝐴 = 𝐵)

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1534   = wceq 1536   ∈ wcel 2105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726

This theorem is referenced by:  eqrdav  2733  abbi  2804  eqabdv  2872  uneq1  4170  unineq  4293  difin2  4306  difsn  4802  eqsndOLD  4835  intmin4  4981  iunconst  5005  iinconst  5006  iuneqconst  5007  dfiun2g  5034  dfiun2gOLD  5035  iindif1  5079  iindif2  5081  iinin2  5082  iunxsng  5094  iunxsngf  5096  opthprc  5752  dmopab2rex  5930  dmxp  5941  epin  6115  inimasn  6177  dmsnopg  6234  dfco2a  6267  iotaeq  6527  imadif  6651  unima  6983  ssimaex  6993  unpreima  7082  respreima  7085  iinpreima  7088  fnsnb  7185  fmptsng  7187  fmptsnd  7188  tpres  7220  iunpw  7789  ordpwsuc  7834  ordsucun  7844  fiun  7965  f1iun  7966  reldm  8067  fimaproj  8158  xpord2pred  8168  xpord3pred  8175  rntpos  8262  onoviun  8381  oarec  8598  iserd  8769  erth  8794  mapdm0  8880  mapfset  8888  ixpiin  8962  boxriin  8978  pw2f1olem  9114  fifo  9469  ordiso2  9552  ttrclse  9764  finacn  10087  acnen  10090  acacni  10178  dfac13  10180  fin23lem26  10362  isf34lem4  10414  axdc3lem2  10488  fpwwe2lem7  10674  fpwwe2lem11  10678  fpwwe2lem12  10679  gch2  10712  gchac  10718  gchina  10736  genpass  11046  1idpr  11066  eqreznegel  12973  ixxun  13399  iccid  13428  difreicc  13520  iccsplit  13521  fzsplit2  13585  fzsn  13602  fzpr  13615  uzsplit  13632  fzdif1  13641  preduz  13686  predfz  13689  fz1isolem  14496  pr2pwpr  14514  isercolllem2  15698  isercoll  15700  bitsmod  16469  bitscmp  16471  saddisj  16498  sadadd  16500  sadass  16504  smupvallem  16516  smueqlem  16523  smumul  16526  gcdcllem2  16533  vdwapun  17007  firest  17478  fncnvimaeqv  18174  mgmhmpropd  18723  mhmpropd  18817  efmnd1bas  18918  subgacs  19191  eqgid  19210  ghmmhmb  19257  ghmpropd  19286  ghmqusnsglem1  19310  ghmquskerlem1  19313  ghmqusker  19317  resscntz  19363  symg1bas  19422  lsmcom2  19687  lsmass  19701  ablnsg  19879  lsmcomx  19888  gsum2d2  20006  subgdmdprd  20068  dprd2d2  20078  2nsgsimpgd  20136  unitpropd  20433  rnghmval2  20460  subsubrng2  20580  subrngpropd  20584  subsubrg2  20615  subrgpropd  20624  rhmpropd  20625  subrgacs  20817  sdrgacs  20818  abvpropd  20852  lssacs  20982  lssats2  21015  lsspropd  21033  lmhmpropd  21089  lbspropd  21115  pzriprnglem10  21518  psdmul  22187  discld  23112  neiptopnei  23155  neiptopreu  23156  restsn  23193  restdis  23201  neitr  23203  restlp  23206  cndis  23314  cnindis  23315  cnpdis  23316  lpcls  23387  hausmapdom  23523  ptpjpre1  23594  tx1cn  23632  tx2cn  23633  hauseqlcld  23669  txkgen  23675  idqtop  23729  tgqtop  23735  acufl  23940  uffix  23944  ufildr  23954  fmfg  23972  rnelfm  23976  fmfnfm  23981  fmid  23983  fmco  23984  flimrest  24006  fclsrest  24047  alexsubALT  24074  tsmsgsum  24162  tsmssubm  24166  tsmsres  24167  tsmsf1o  24168  xpsdsval  24406  blpnf  24422  blin  24446  blres  24456  xmetec  24459  imasf1obl  24516  imasf1oxms  24517  prdsbl  24519  metrest  24552  psmetutop  24595  restmetu  24598  dscopn  24601  cnbl0  24809  bl2ioo  24827  xrtgioo  24841  cncfmet  24948  icoopnst  24982  iocopnst  24983  cldcss2  25489  iunmbl2  25605  mbfmulc2lem  25695  mbfmax  25697  ismbf3d  25702  mbfimaopnlem  25703  mbfaddlem  25708  mbfsup  25712  i1f1lem  25737  i1faddlem  25741  i1fmullem  25742  i1fmulclem  25751  i1fres  25754  mbfi1fseqlem4  25767  limcdif  25925  limcnlp  25927  limcflf  25930  limcres  25935  limcun  25944  ply1remlem  26218  fta1glem2  26222  plypf1  26265  ofmulrt  26337  plyremlem  26360  aannenlem1  26384  gausslemma2dlem1a  27423  oldlim  27939  tglineelsb2  28654  tglinecom  28657  ushgredgedg  29260  ushgredgedgloop  29262  nbumgrvtx  29377  nbusgrvtxm1uvtx  29436  vdiscusgr  29563  wspniunwspnon  29952  rusgrnumwwlkb0  30000  clwwlknscsh  30090  clwwlknun  30140  eupth2lems  30266  fusgr2wsp2nb  30362  fusgreg2wsp  30364  ubthlem1  30898  ocin  31324  shscom  31347  spansncol  31596  iunsnima  32637  iunsnima2  32638  nfpconfp  32648  unipreima  32659  2ndimaxp  32662  fdifsupp  32699  suppiniseg  32700  ressupprn  32704  1stpreimas  32720  1stpreima  32721  2ndpreima  32722  fpwrelmapffslem  32749  iocinioc2  32787  nndiffz1  32794  fzsplit3  32801  swrdrn3  32924  cntzun  33053  cntzsnid  33054  ecxpid  33368  qsxpid  33369  lindspropd  33390  lsmsnpridl  33405  lsmssass  33409  grplsm0l  33410  grplsmid  33411  nsgqusf1olem2  33421  nsgqusf1olem3  33422  crngmxidl  33476  opprlidlabs  33492  rprmirredb  33539  ressply1mon1p  33572  irngnzply1  33705  smatrcl  33756  qtophaus  33796  locfinreflem  33800  rspectopn  33827  zarclsiin  33831  rhmpreimacnlem  33844  prsdm  33874  prsrn  33875  indpi1  34000  indf1ofs  34006  1stmbfm  34241  2ndmbfm  34242  mbfmcnt  34249  eulerpartlemgh  34359  dstfrvunirn  34455  reprsuc  34608  reprpmtf1o  34619  satfvsucsuc  35349  dmopab3rexdif  35389  cbvabdavw  36238  neifg  36353  filnetlem4  36363  ontgval  36413  bj-gabima  36922  bj-restsn  37064  bj-rest10  37070  bj-restpw  37074  bj-restuni  37079  mptsnunlem  37320  finxpsuclem  37379  wl-clabtv  37577  wl-clabt  37578  poimirlem16  37622  poimirlem19  37625  poimirlem23  37629  poimirlem27  37633  heicant  37641  istotbnd3  37757  sstotbnd  37761  ismtyima  37789  heibor  37807  divrngidl  38014  eccnvep  38263  ecxrn  38368  eqvrelth  38592  disjlem19  38782  prtlem19  38859  prter2  38862  lkrsc  39078  lshpkr  39098  paddvaln0N  39783  paddval0  39792  diaglbN  41037  cdlemm10N  41100  lcfrvalsnN  41523  lcfrlem9  41532  lcdlss  41601  mapd1o  41630  mapd0  41647  hlhillcs  41944  grpods  42175  unitscyglem2  42177  sn-iotalem  42238  fnsnbt  42249  fsuppind  42576  mzpmfp  42734  lzunuz  42755  fz1eqin  42756  jm2.23  42984  pw2f1ocnv  43025  dfacbasgrp  43096  nnoeomeqom  43301  oadif1lem  43368  oadif1  43369  fzunt  43444  fzuntd  43445  fzunt1d  43446  fzuntgd  43447  inintabd  43568  cnvcnvintabd  43589  cnvintabd  43592  rfcnpre3  44970  rfcnpre4  44971  iindif2f  45102  rnmptpr  45119  iccshift  45470  iocopn  45472  iooshift  45474  iccintsng  45475  icoopn  45477  limcdm0  45573  limcresiooub  45597  limcresioolb  45598  fperdvper  45874  itgperiod  45936  fourierdlem32  46094  fourierdlem33  46095  fourierdlem48  46109  fourierdlem49  46110  fourierdlem81  46142  fsetsniunop  46998  elsetpreimafvrab  47318  iccpartiun  47358  dfclnbgr6  47779  dfnbgr6  47780  uhgrimisgrgric  47836  clnbgrgrim  47839  stgredgiun  47860  gpgnbgrvtx0  47964  gpgnbgrvtx1  47965  itsclinecirc0in  48624  i0oii  48715  io1ii  48716  thincmon  48833  thincepi  48834  grptcmon  48901  grptcepi  48902