Theorem eqrdv 2758

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 1960	. 2 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3		dfcleq 2753	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4	2, 3	sylibr 237	1 ⊢ (𝜑 → 𝐴 = 𝐵)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1568   = wceq 1570   ∈ wcel 2145

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752

This theorem is used by:  eqrdav  2759  abbi  2825  eqabdv  2893  uneq1  4108  unineq  4234  difin2  4247  difsn  4761  intmin4  4937  intprg  4941  iunconst  4961  iinconst  4962  iuneqconst  4963  dfiun2g  4988  iindif1  5035  iindif2  5037  iinin2  5038  iunxsng  5050  iunxsngf  5052  opthprc  5719  dmopab2rex  5901  dmxp  5913  epin  6091  inimasn  6147  dmsnopg  6209  dfco2a  6242  iotaeq  6501  imadif  6617  unima  6953  ssimaex  6963  unpreima  7055  respreima  7058  iinpreima  7062  fnsnbg  7162  fnsnbOLD  7164  fmptsng  7166  fmptsnd  7167  tpres  7200  iunpw  7770  ordpwsuc  7811  ordsucun  7821  fiun  7940  f1iun  7941  reldm  8041  fimaproj  8133  xpord2pred  8143  xpord3pred  8150  rntpos  8237  onoviun  8332  oarec  8549  iserd  8723  erth  8751  mapdm0  8841  mapfset  8851  ixpiin  8931  boxriin  8947  pw2f1olem  9079  fifo  9402  ordiso2  9487  ttrclse  9706  finacn  10053  acnen  10056  acacni  10143  dfac13  10145  fin23lem26  10327  isf34lem4  10379  axdc3lem2  10453  fpwwe2lem7  10646  fpwwe2lem11  10650  fpwwe2lem12  10651  gch2  10684  gchac  10690  gchina  10708  genpass  11018  1idpr  11038  indpi1  12256  eqreznegel  12983  ixxun  13414  iccid  13443  difreicc  13537  iccsplit  13538  fzsplit2  13604  fzsn  13621  fzpr  13634  uzsplit  13651  fzdif1  13660  preduz  13705  predfz  13708  fz1isolem  14526  pr2pwpr  14544  swrdrn3  14722  isercolllem2  15753  isercoll  15755  bitsmod  16526  bitscmp  16528  saddisj  16555  sadadd  16557  sadass  16561  smupvallem  16573  smueqlem  16580  smumul  16583  gcdcllem2  16590  vdwapun  17066  firest  17517  fncnvimaeqv  18208  mgmhmpropd  18800  mhmpropd  18900  efmnd1bas  19002  subgacs  19284  ecxpid  19299  qsxpid  19300  eqgid  19305  ghmmhmb  19354  ghmpropd  19383  ghmqusnsglem1  19407  ghmquskerlem1  19410  ghmqusker  19414  resscntz  19460  symg1bas  19518  lsmcom2  19782  lsmass  19796  ablnsg  19974  lsmcomx  19983  gsum2d2  20101  subgdmdprd  20163  dprd2d2  20173  2nsgsimpgd  20231  unitpropd  20558  rnghmval2  20585  subsubrng2  20726  subrngpropd  20730  subsubrg2  20761  subrgpropd  20770  rhmpropd  20771  subrgacs  20966  sdrgacs  20967  abvpropd  21001  lssacs  21151  lssats2  21184  lsspropd  21201  lmhmpropd  21257  lbspropd  21283  pzriprnglem10  21703  psdmul  22394  discld  23314  neiptopnei  23357  neiptopreu  23358  restsn  23395  restdis  23403  neitr  23405  restlp  23408  cndis  23516  cnindis  23517  cnpdis  23518  lpcls  23589  hausmapdom  23726  ptpjpre1  23797  tx1cn  23835  tx2cn  23836  hauseqlcld  23872  txkgen  23878  idqtop  23932  tgqtop  23938  acufl  24143  uffix  24147  ufildr  24157  fmfg  24175  rnelfm  24179  fmfnfm  24184  fmid  24186  fmco  24187  flimrest  24209  fclsrest  24250  alexsubALT  24277  tsmsgsum  24365  tsmssubm  24369  tsmsres  24370  tsmsf1o  24371  xpsdsval  24607  blpnf  24623  blin  24647  blres  24657  xmetec  24660  imasf1obl  24714  imasf1oxms  24715  prdsbl  24717  metrest  24750  psmetutop  24793  restmetu  24796  dscopn  24799  cnbl0  24999  bl2ioo  25018  xrtgioo  25033  cncfmet  25137  icoopnst  25167  iocopnst  25168  cldcss2  25670  iunmbl2  25785  mbfmulc2lem  25875  mbfmax  25877  ismbf3d  25882  mbfimaopnlem  25883  mbfaddlem  25888  mbfsup  25892  i1f1lem  25917  i1faddlem  25921  i1fmullem  25922  i1fmulclem  25930  i1fres  25933  mbfi1fseqlem4  25946  limcdif  26103  limcnlp  26105  limcflf  26108  limcres  26113  limcun  26122  ply1remlem  26390  fta1glem2  26394  plypf1  26438  ofmulrt  26509  plyremlem  26534  rnplynfin  26539  aannenlem1  26564  gausslemma2dlem1a  27601  oldlim  28152  negleft  28323  negright  28324  tglineelsb2  28979  tglinecom  28982  angmgmaddcpbl  29269  ushgredgedg  29689  ushgredgedgloop  29691  nbumgrvtx  29806  nbusgrvtxm1uvtx  29865  vdiscusgr  29991  wspniunwspnon  30391  rusgrnumwwlkb0  30442  clwwlknscsh  30532  clwwlknun  30582  eupth2lems  30718  fusgr2wsp2nb  30814  fusgreg2wsp  30816  ubthlem1  31351  ocin  31777  shscom  31800  spansncol  32049  iunsnima  33091  iunsnima2  33092  nfpconfp  33105  unipreima  33116  2ndimaxp  33119  fdifsupp  33157  suppiniseg  33158  ressupprn  33162  1stpreimas  33178  1stpreima  33179  2ndpreima  33180  fpwrelmapffslem  33203  iocinioc2  33250  nndiffz1  33257  fzsplit3  33264  indf1ofs  33312  cntzun  33519  cntzsnid  33520  cntrval2  33611  lindspropd  33816  lsmsnpridl  33829  lsmssass  33831  grplsm0l  33832  grplsmid  33833  nsgqusf1olem2  33843  nsgqusf1olem3  33844  crngmxidl  33872  opprlidlabs  33887  rprmirredb  33942  ressply1mon1p  33978  fldextrspunlsp  34184  irngnzply1  34201  smatrcl  34306  qtophaus  34346  locfinreflem  34350  rspectopn  34377  zarclsiin  34381  rhmpreimacnlem  34394  prsdm  34424  prsrn  34425  1stmbfm  34771  2ndmbfm  34772  mbfmcnt  34779  eulerpartlemgh  34889  dstfrvunirn  34986  reprsuc  35123  reprpmtf1o  35134  satfvsucsuc  35944  dmopab3rexdif  35984  cbvabdavw  36876  neifg  36990  filnetlem4  37000  ontgval  37050  bj-gabima  37684  bj-restsn  37832  bj-rest10  37838  bj-restpw  37842  bj-restuni  37847  mptsnunlem  38092  finxpsuclem  38151  wl-clabtv  38349  wl-clabt  38350  poimirlem16  38385  poimirlem19  38388  poimirlem23  38392  poimirlem27  38396  heicant  38404  istotbnd3  38521  sstotbnd  38525  ismtyima  38553  heibor  38571  divrngidl  38778  eccnvep  39036  ecxrn  39154  eqvrelth  39443  disjlem19  39652  prtlem19  39751  prter2  39754  lkrsc  39970  lshpkr  39990  paddvaln0N  40674  paddval0  40683  diaglbN  41928  cdlemm10N  41991  lcfrvalsnN  42414  lcfrlem9  42423  lcdlss  42492  mapd1o  42521  mapd0  42538  hlhillcs  42831  grpods  43060  unitscyglem2  43062  sn-iotalem  43091  fsuppind  43436  mzpmfp  43592  lzunuz  43613  fz1eqin  43614  jm2.23  43837  pw2f1ocnv  43878  dfacbasgrp  43949  nnoeomeqom  44153  oadif1lem  44220  oadif1  44221  fzunt  44295  fzuntd  44296  fzunt1d  44297  fzuntgd  44298  inintabd  44419  cnvcnvintabd  44440  cnvintabd  44443  rfcnpre3  45867  rfcnpre4  45868  iindif2f  45992  rnmptpr  46009  iccshift  46348  iocopn  46350  iooshift  46352  iccintsng  46353  icoopn  46355  limcdm0  46448  limcresiooub  46470  limcresioolb  46471  fperdvper  46747  itgperiod  46809  fourierdlem32  46967  fourierdlem33  46968  fourierdlem48  46982  fourierdlem49  46983  fourierdlem81  47015  fsetsniunop  47937  elsetpreimafvrab  48294  iccpartiun  48334  dfclnbgr6  48772  dfnbgr6  48773  uhgrimisgrgric  48847  clnbgrgrim  48850  stgredgiun  48874  gpgnbgrvtx0  48990  gpgnbgrvtx1  48991  itsclinecirc0in  49705  i0oii  49846  io1ii  49847  sectpropd  49963  invpropd  49965  isopropd  49967  cicpropd  49976  uobffth  50144  uobeqw  50145  natoppfb  50157  oppc1stflem  50213  thincmon  50359  thincepi  50360  termfucterm  50470  grptcmon  50519  grptcepi  50520  lanval2  50553  ranval2  50556  ranval3  50557