Theorem eqrdv 2761

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

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1568   = wceq 1570   ∈ wcel 2143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755

This theorem is referenced by:  eqrdav  2762  abbi  2828  eqabdv  2896  uneq1  4115  unineq  4241  difin2  4254  difsn  4766  intmin4  4942  intprg  4946  iunconst  4966  iinconst  4967  iuneqconst  4968  dfiun2g  4994  iindif1  5041  iindif2  5043  iinin2  5044  iunxsng  5056  iunxsngf  5058  opthprc  5725  dmopab2rex  5907  dmxp  5919  epin  6097  inimasn  6153  dmsnopg  6214  dfco2a  6247  iotaeq  6504  imadif  6620  unima  6956  ssimaex  6966  unpreima  7058  respreima  7061  iinpreima  7064  fnsnbg  7162  fnsnbOLD  7164  fmptsng  7166  fmptsnd  7167  tpres  7199  iunpw  7766  ordpwsuc  7807  ordsucun  7817  fiun  7936  f1iun  7937  reldm  8037  fimaproj  8127  xpord2pred  8137  xpord3pred  8144  rntpos  8231  onoviun  8326  oarec  8543  iserd  8717  erth  8745  mapdm0  8835  mapfset  8843  ixpiin  8918  boxriin  8934  pw2f1olem  9065  fifo  9388  ordiso2  9473  ttrclse  9692  finacn  10030  acnen  10033  acacni  10120  dfac13  10122  fin23lem26  10304  isf34lem4  10356  axdc3lem2  10430  fpwwe2lem7  10617  fpwwe2lem11  10621  fpwwe2lem12  10622  gch2  10655  gchac  10661  gchina  10679  genpass  10989  1idpr  11009  indpi1  12227  eqreznegel  12953  ixxun  13383  iccid  13412  difreicc  13506  iccsplit  13507  fzsplit2  13573  fzsn  13590  fzpr  13603  uzsplit  13620  fzdif1  13629  preduz  13674  predfz  13677  fz1isolem  14494  pr2pwpr  14512  isercolllem2  15713  isercoll  15715  bitsmod  16489  bitscmp  16491  saddisj  16518  sadadd  16520  sadass  16524  smupvallem  16536  smueqlem  16543  smumul  16546  gcdcllem2  16553  vdwapun  17029  firest  17480  fncnvimaeqv  18171  mgmhmpropd  18751  mhmpropd  18845  efmnd1bas  18947  subgacs  19222  ecxpid  19237  qsxpid  19238  eqgid  19243  ghmmhmb  19292  ghmpropd  19321  ghmqusnsglem1  19345  ghmquskerlem1  19348  ghmqusker  19352  resscntz  19398  symg1bas  19456  lsmcom2  19720  lsmass  19734  ablnsg  19912  lsmcomx  19921  gsum2d2  20039  subgdmdprd  20101  dprd2d2  20111  2nsgsimpgd  20169  unitpropd  20495  rnghmval2  20522  subsubrng2  20663  subrngpropd  20667  subsubrg2  20698  subrgpropd  20707  rhmpropd  20708  subrgacs  20903  sdrgacs  20904  abvpropd  20938  lssacs  21088  lssats2  21121  lsspropd  21138  lmhmpropd  21194  lbspropd  21220  pzriprnglem10  21640  psdmul  22329  discld  23246  neiptopnei  23289  neiptopreu  23290  restsn  23327  restdis  23335  neitr  23337  restlp  23340  cndis  23448  cnindis  23449  cnpdis  23450  lpcls  23521  hausmapdom  23657  ptpjpre1  23728  tx1cn  23766  tx2cn  23767  hauseqlcld  23803  txkgen  23809  idqtop  23863  tgqtop  23869  acufl  24074  uffix  24078  ufildr  24088  fmfg  24106  rnelfm  24110  fmfnfm  24115  fmid  24117  fmco  24118  flimrest  24140  fclsrest  24181  alexsubALT  24208  tsmsgsum  24296  tsmssubm  24300  tsmsres  24301  tsmsf1o  24302  xpsdsval  24538  blpnf  24554  blin  24578  blres  24588  xmetec  24591  imasf1obl  24645  imasf1oxms  24646  prdsbl  24648  metrest  24681  psmetutop  24724  restmetu  24727  dscopn  24730  cnbl0  24930  bl2ioo  24949  xrtgioo  24964  cncfmet  25068  icoopnst  25098  iocopnst  25099  cldcss2  25601  iunmbl2  25716  mbfmulc2lem  25806  mbfmax  25808  ismbf3d  25813  mbfimaopnlem  25814  mbfaddlem  25819  mbfsup  25823  i1f1lem  25848  i1faddlem  25852  i1fmullem  25853  i1fmulclem  25861  i1fres  25864  mbfi1fseqlem4  25877  limcdif  26035  limcnlp  26037  limcflf  26040  limcres  26045  limcun  26054  ply1remlem  26322  fta1glem2  26326  plypf1  26369  ofmulrt  26440  plyremlem  26465  aannenlem1  26491  gausslemma2dlem1a  27529  oldlim  28080  negleft  28251  negright  28252  tglineelsb2  28905  tglinecom  28908  ushgredgedg  29579  ushgredgedgloop  29581  nbumgrvtx  29696  nbusgrvtxm1uvtx  29755  vdiscusgr  29881  wspniunwspnon  30272  rusgrnumwwlkb0  30323  clwwlknscsh  30413  clwwlknun  30463  eupth2lems  30589  fusgr2wsp2nb  30685  fusgreg2wsp  30687  ubthlem1  31222  ocin  31648  shscom  31671  spansncol  31920  iunsnima  32963  iunsnima2  32964  nfpconfp  32977  unipreima  32988  2ndimaxp  32991  fdifsupp  33030  suppiniseg  33031  ressupprn  33035  1stpreimas  33051  1stpreima  33052  2ndpreima  33053  fpwrelmapffslem  33077  iocinioc2  33124  nndiffz1  33131  fzsplit3  33138  indf1ofs  33186  swrdrn3  33275  cntzun  33399  cntzsnid  33400  cntrval2  33491  lindspropd  33696  lsmsnpridl  33709  lsmssass  33711  grplsm0l  33712  grplsmid  33713  nsgqusf1olem2  33723  nsgqusf1olem3  33724  crngmxidl  33752  opprlidlabs  33767  rprmirredb  33822  ressply1mon1p  33858  fldextrspunlsp  34064  irngnzply1  34081  smatrcl  34186  qtophaus  34226  locfinreflem  34230  rspectopn  34257  zarclsiin  34261  rhmpreimacnlem  34274  prsdm  34304  prsrn  34305  1stmbfm  34650  2ndmbfm  34651  mbfmcnt  34658  eulerpartlemgh  34768  dstfrvunirn  34865  reprsuc  35002  reprpmtf1o  35013  satfvsucsuc  35857  dmopab3rexdif  35897  cbvabdavw  36768  neifg  36882  filnetlem4  36892  ontgval  36942  bj-gabima  37576  bj-restsn  37724  bj-rest10  37730  bj-restpw  37734  bj-restuni  37739  mptsnunlem  37984  finxpsuclem  38043  wl-clabtv  38241  wl-clabt  38242  poimirlem16  38287  poimirlem19  38290  poimirlem23  38294  poimirlem27  38298  heicant  38306  istotbnd3  38422  sstotbnd  38426  ismtyima  38454  heibor  38472  divrngidl  38679  eccnvep  38937  ecxrn  39055  eqvrelth  39344  disjlem19  39553  prtlem19  39652  prter2  39655  lkrsc  39871  lshpkr  39891  paddvaln0N  40575  paddval0  40584  diaglbN  41829  cdlemm10N  41892  lcfrvalsnN  42315  lcfrlem9  42324  lcdlss  42393  mapd1o  42422  mapd0  42439  hlhillcs  42732  grpods  42961  unitscyglem2  42963  sn-iotalem  42992  fsuppind  43322  mzpmfp  43478  lzunuz  43499  fz1eqin  43500  jm2.23  43723  pw2f1ocnv  43764  dfacbasgrp  43835  nnoeomeqom  44039  oadif1lem  44106  oadif1  44107  fzunt  44181  fzuntd  44182  fzunt1d  44183  fzuntgd  44184  inintabd  44305  cnvcnvintabd  44326  cnvintabd  44329  rfcnpre3  45753  rfcnpre4  45754  iindif2f  45878  rnmptpr  45895  iccshift  46234  iocopn  46236  iooshift  46238  iccintsng  46239  icoopn  46241  limcdm0  46334  limcresiooub  46356  limcresioolb  46357  fperdvper  46633  itgperiod  46695  fourierdlem32  46853  fourierdlem33  46854  fourierdlem48  46868  fourierdlem49  46869  fourierdlem81  46901  fsetsniunop  47786  elsetpreimafvrab  48143  iccpartiun  48183  dfclnbgr6  48621  dfnbgr6  48622  uhgrimisgrgric  48696  clnbgrgrim  48699  stgredgiun  48723  gpgnbgrvtx0  48839  gpgnbgrvtx1  48840  itsclinecirc0in  49555  i0oii  49698  io1ii  49699  sectpropd  49815  invpropd  49817  isopropd  49819  cicpropd  49828  uobffth  49996  uobeqw  49997  natoppfb  50009  oppc1stflem  50065  thincmon  50211  thincepi  50212  termfucterm  50322  grptcmon  50371  grptcepi  50372  lanval2  50405  ranval2  50408  ranval3  50409