MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eleq2 Unicode version

Theorem eleq2 2344
Description: Equality implies equivalence of membership. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
eleq2  |-  ( A  =  B  ->  ( C  e.  A  <->  C  e.  B ) )

Proof of Theorem eleq2
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 dfcleq 2277 . . . . . 6  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
21biimpi 186 . . . . 5  |-  ( A  =  B  ->  A. x
( x  e.  A  <->  x  e.  B ) )
3219.21bi 1794 . . . 4  |-  ( A  =  B  ->  (
x  e.  A  <->  x  e.  B ) )
43anbi2d 684 . . 3  |-  ( A  =  B  ->  (
( x  =  C  /\  x  e.  A
)  <->  ( x  =  C  /\  x  e.  B ) ) )
54exbidv 1612 . 2  |-  ( A  =  B  ->  ( E. x ( x  =  C  /\  x  e.  A )  <->  E. x
( x  =  C  /\  x  e.  B
) ) )
6 df-clel 2279 . 2  |-  ( C  e.  A  <->  E. x
( x  =  C  /\  x  e.  A
) )
7 df-clel 2279 . 2  |-  ( C  e.  B  <->  E. x
( x  =  C  /\  x  e.  B
) )
85, 6, 73bitr4g 279 1  |-  ( A  =  B  ->  ( C  e.  A  <->  C  e.  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358   A.wal 1527   E.wex 1528    = wceq 1623    e. wcel 1684
This theorem is referenced by:  eleq12  2345  eleq2i  2347  eleq2d  2350  nelneq2  2382  dvelimdc  2439  nelne1  2535  neleq2  2538  raleqf  2732  rexeqf  2733  reueq1f  2734  rmoeq1f  2735  rabeqf  2781  clel3g  2905  clel4  2907  sbcel2gv  3051  sbnfc2  3141  difeq2  3288  uneq1  3322  ineq1  3363  unineq  3419  n0i  3460  disjel  3501  elif  3599  sneqr  3780  preqr1  3786  preq12b  3788  prel12  3789  elunii  3832  eluniab  3839  ssuni  3849  elinti  3871  elintab  3873  intss1  3877  intmin  3882  intab  3892  iineq2  3922  dfiin2g  3936  breq  4025  axrep1  4132  zfrepclf  4137  axsep2  4142  zfauscl  4143  inuni  4173  elALT  4218  rext  4222  intid  4231  opth1  4244  opthwiener  4268  ordtri1  4425  ordtri3  4428  nsuceq0  4472  suctr  4475  trsuc2OLD  4477  ordnbtwn  4483  snnex  4524  uniuni  4527  iunpw  4570  oneqmin  4596  onuninsuci  4631  nlimsucg  4633  limomss  4661  nnlim  4669  peano5  4679  xpeq1  4703  xpeq2  4704  opthprc  4736  funopg  5286  dffv2  5592  dffo4  5676  elunirnALT  5779  f1oiso  5848  mpt2eq123  5907  ndmovg  6003  unielxp  6158  cnvf1o  6217  canth  6294  eusvobj2  6337  smoel  6377  smo11  6381  tz7.44-2  6420  oawordeulem  6552  oaordex  6556  omordi  6564  oneo  6579  oeordi  6585  oeoa  6595  oeoe  6597  nnmordi  6629  nnaordex  6636  omabs  6645  nnneo  6649  omsmolem  6651  elqsn0  6728  qsel  6738  mapsn  6809  undifixp  6852  boxriin  6858  boxcutc  6859  fineqvlem  7077  fineqv  7078  pssnn  7081  fissuni  7160  dffi2  7176  inficl  7178  dffi3  7184  wofib  7260  zfregcl  7308  suc11reg  7320  inf0  7322  inf3lem2  7330  inf3lem3  7331  infeq5i  7337  axinf2  7341  dfom3  7348  elom3  7349  noinfepOLD  7361  cantnfle  7372  oemapvali  7386  cantnflem1c  7389  cantnflem1  7391  en3lplem1  7416  en3lp  7418  tc2  7427  r1sdom  7446  rankwflemb  7465  rankval3b  7498  rankunb  7522  rankuni2b  7525  tcrank  7554  cardlim  7605  cardprclem  7612  infxpenlem  7641  alephnbtwn  7698  alephordi  7701  cardaleph  7716  alephfp  7735  alephval3  7737  aceq1  7744  aceq2  7746  dfac3  7748  dfac5lem2  7751  dfac5lem4  7753  dfac2  7757  kmlem2  7777  kmlem4  7779  coflim  7887  cfsmolem  7896  fin23lem30  7968  isf32lem2  7980  isf34lem4  8003  axdc2lem  8074  axdc3lem2  8077  axdc3lem4  8079  axdc4lem  8081  zorn2lem7  8129  axdclem  8146  brdom7disj  8156  brdom6disj  8157  axpowndlem3  8221  winainflem  8315  iswun  8326  eltskg  8372  inar1  8397  elgrug  8414  inaprc  8458  eltskm  8465  addnidpi  8525  indpi  8531  nqereu  8553  elnp  8611  elnpi  8612  genpnnp  8629  ltaddpr  8658  dfnn2  9759  dfnn3  9760  dfuzi  10102  uz11  10250  om2uzlti  11013  axdc4uz  11045  hashbclem  11390  hashf1lem2  11394  rpnnen2lem1  12493  rpnnen2lem2  12494  sadcp1  12646  ismre  13492  isacs  13553  mreclat  14290  issubm  14425  cycsubg  14645  isnsg  14646  subgacs  14652  nsgacs  14653  resghm  14699  ghmeql  14705  gsumzsplit  15206  pgpfac1lem1  15309  pgpfac1lem5  15314  pgpfac1  15315  issubrg  15545  islss  15692  lssacs  15724  lspsneq0  15769  lmhmeql  15812  lspdisjb  15879  lidl1el  15970  lidldvgen  16007  mplcoe1  16209  mplcoe2  16211  istopg  16641  fiinbas  16690  topbas  16710  ppttop  16744  pptbas  16745  epttop  16746  elcls  16810  clsndisj  16812  elcls3  16820  iscldtop  16832  restbas  16889  restntr  16912  pnfnei  16950  mnfnei  16951  cnpimaex  16986  lmcvg  16992  cncnpi  17007  cnconst2  17011  cnprest  17017  cnprest2  17018  cnpdis  17021  lmss  17026  lmff  17029  cnt0  17074  ist1-3  17077  cnhaus  17082  isreg2  17105  dishaus  17110  ordthauslem  17111  cmpsublem  17126  cmpsub  17127  cmpcld  17129  hauscmplem  17133  uncon  17155  concompid  17157  concompcon  17158  concompss  17159  1stcfb  17171  1stcrest  17179  2ndcctbss  17181  2ndcomap  17184  dis2ndc  17186  1stcelcls  17187  llyeq  17196  nllyeq  17197  restnlly  17208  restlly  17209  islly2  17210  lly1stc  17222  dislly  17223  hauspwdom  17227  llycmpkgen2  17245  txbas  17262  eltx  17263  ptpjopn  17306  ptclsg  17309  dfac14lem  17311  txcnp  17314  ptcnplem  17315  ptcnp  17316  txlly  17330  pthaus  17332  txtube  17334  txhaus  17341  txlm  17342  tx1stc  17344  txkgen  17346  xkohaus  17347  xkopt  17349  xkococnlem  17353  tgqtop  17403  kqfvima  17421  kqt0lem  17427  isr0  17428  r0cld  17429  regr1lem  17430  kqreglem1  17432  kqreglem2  17433  reghmph  17484  fbssfi  17532  isfil  17542  filuni  17580  isufil  17598  isufil2  17603  uffix  17616  fixufil  17617  uffixfr  17618  uffixsn  17620  rnelfm  17648  flimopn  17670  flimrest  17678  flimcls  17680  flftg  17691  txflf  17701  fclsopni  17710  fclsrest  17719  fclscf  17720  fcfnei  17730  alexsublem  17738  alexsubALTlem3  17743  alexsubALT  17745  tmdgsum2  17779  symgtgp  17784  subgntr  17789  opnsubg  17790  tgpconcompeqg  17794  ghmcnp  17797  tgpt0  17801  divstgpopn  17802  tsmsi  17816  tsmssubm  17825  tsmssplit  17834  blss  17972  blssex  17973  neibl  18047  blcld  18051  metss  18054  methaus  18066  met1stc  18067  met2ndci  18068  metrest  18070  prdsxmslem2  18075  metcnp3  18086  dscopn  18096  idnghm  18252  qdensere  18279  tgioo  18302  tgqioo  18306  zdis  18322  xrge0tsms  18339  cnheibor  18453  lmmbr  18684  bcthlem4  18749  ovolicc2lem5  18880  dyadmbllem  18954  i1fd  19036  itg11  19046  itg2gt0  19115  itgeq1f  19126  bddmulibl  19193  ellimc2  19227  limcnlp  19228  ellimc3  19229  limcflf  19231  limciun  19244  lhop1lem  19360  ig1pdvds  19562  plycpn  19669  aannenlem2  19709  efopn  20005  xrlimcnp  20263  wilthlem2  20307  wilthlem3  20308  wilth  20309  lpni  20846  rngoueqz  21097  issh  21787  pjoc1  22013  h1dn0  22131  spansneleqi  22148  nonbooli  22230  pjch  22273  pjnel  22305  cdjreui  23012  ballotlem7  23094  rexunirn  23140  abfmpunirn  23216  abfmpeld  23218  abfmpel  23219  tpr2rico  23296  lmxrge0  23375  xrge0tsmsd  23382  issiga  23472  isrnsigaOLD  23473  isrnsiga  23474  ismbfm  23557  isanmbfm  23561  dya2iocseg  23579  indval  23597  erdszelem1  23722  kur14lem9  23745  cnllyscon  23776  cvmcov  23794  cvmsss2  23805  cvmcov2  23806  cvmseu  23807  cvmsiota  23808  cvmopnlem  23809  cvmliftlem15  23829  vdgr1a  23897  eupath2lem1  23901  rtrclreclem.trans  24043  untelirr  24054  untsucf  24056  dfon2lem4  24142  dfon2lem7  24145  dfon2lem9  24147  soseq  24254  frrlem4  24284  frrlem5e  24289  frrlem11  24293  nodenselem8  24342  nocvxminlem  24344  nofulllem5  24360  dfiota3  24462  funpartfun  24481  funpartfv  24483  tfrqfree  24489  linethru  24776  hilbert1.1  24777  hilbert1.2  24778  rankelg  24798  elhf2  24805  cbicp  25166  prl2  25169  preoref22  25229  defse3  25272  prodeq3ii  25308  isidlNEW  25446  glmrngo  25482  elioo1t3  25502  nsn  25530  iscnp4  25563  prdnei  25573  bwt2  25592  altretop  25600  tcnvec  25690  elcarelcl  25906  prismorcset  25914  morcatset1  25915  isgraphmrph2  25924  domcatfun  25925  domcatsetval2  25929  domcatval2  25931  codcatfun  25934  codcatval2  25937  prismorcset3  25938  rocatval2  25960  setiscat  25979  indcls2  25996  clscnc  26010  pfsubkl  26047  elhaltdp2  26068  tethpnc2  26071  lineval42  26080  lineval22  26082  isibg2  26110  isibcg  26191  fneint  26277  finlocfin  26299  locfindis  26305  comppfsc  26307  neibastop2lem  26309  cover2  26358  isbnd2  26507  prdstotbnd  26518  heibor1lem  26533  grpokerinj  26575  isidl  26639  1idl  26651  0rngo  26652  ispridl  26659  smprngopr  26677  isfldidl  26693  isdmn3  26699  elmzpcl  26804  diophren  26896  dford3lem2  27120  ttac  27129  pw2f1ocnv  27130  wepwsolem  27138  kelac1  27161  f1otrspeq  27390  pmtrval  27394  sdrgacs  27509  expgrowthi  27550  dvconstbi  27551  elunif  27687  fnchoice  27700  stoweidlem27  27776  stoweidlem35  27784  stoweidlem46  27795  stoweidlem48  27797  stoweidlem52  27801  stoweidlem59  27808  funressnfv  27991  fnbrafvb  28016  afvco2  28037  ndmaovg  28044  aovmpt4g  28061  uvtx01vtx  28164  uvtxnbgravtx  28167  tratrb  28299  suctrALT2VD  28612  suctrALT2  28613  en3lplem1VD  28619  en3lpVD  28621  tratrbVD  28637  suctrALTcf  28698  suctrALTcfVD  28699  suctrALT3  28700  unisnALT  28702  suctrALT4  28704  bnj145  28755  bnj216  28760  bnj563  28772  bnj956  28808  bnj545  28927  bnj548  28929  bnj570  28937  bnj900  28961  bnj929  28968  bnj964  28975  bnj983  28983  bnj1001  28990  bnj1145  29023  bnj1398  29064  bnj1498  29091  lsateln0  29185  ispsubsp  29934  linepsubN  29941  elpcliN  30082  dvh3dim3N  31639  dochsnnz  31640  mapdindp3  31912
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-cleq 2276  df-clel 2279
  Copyright terms: Public domain W3C validator