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

Theorem eleq2 2441
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 2374 . . . . . 6  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
21biimpi 187 . . . . 5  |-  ( A  =  B  ->  A. x
( x  e.  A  <->  x  e.  B ) )
3219.21bi 1766 . . . 4  |-  ( A  =  B  ->  (
x  e.  A  <->  x  e.  B ) )
43anbi2d 685 . . 3  |-  ( A  =  B  ->  (
( x  =  C  /\  x  e.  A
)  <->  ( x  =  C  /\  x  e.  B ) ) )
54exbidv 1633 . 2  |-  ( A  =  B  ->  ( E. x ( x  =  C  /\  x  e.  A )  <->  E. x
( x  =  C  /\  x  e.  B
) ) )
6 df-clel 2376 . 2  |-  ( C  e.  A  <->  E. x
( x  =  C  /\  x  e.  A
) )
7 df-clel 2376 . 2  |-  ( C  e.  B  <->  E. x
( x  =  C  /\  x  e.  B
) )
85, 6, 73bitr4g 280 1  |-  ( A  =  B  ->  ( C  e.  A  <->  C  e.  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359   A.wal 1546   E.wex 1547    = wceq 1649    e. wcel 1717
This theorem is referenced by:  eleq12  2442  eleq2i  2444  eleq2d  2447  nelneq2  2479  dvelimdc  2536  nelne1  2632  neleq2  2637  raleqf  2836  rexeqf  2837  reueq1f  2838  rmoeq1f  2839  rabeqf  2885  clel3g  3009  clel4  3011  sbcel2gv  3157  sbnfc2  3245  difeq2  3395  uneq1  3430  ineq1  3471  unineq  3527  n0i  3569  disjel  3610  elif  3709  exsnrex  3784  sneqr  3901  preqr1  3907  preq12b  3909  prel12  3910  elunii  3955  eluniab  3962  ssuni  3972  elinti  3994  elintab  3996  intss1  4000  intmin  4005  intab  4015  iineq2  4045  dfiin2g  4059  breq  4148  zfrepclf  4260  axsep2  4265  zfauscl  4266  inuni  4296  elALT  4341  rext  4346  intid  4355  opth1  4368  opthwiener  4392  ordtri1  4548  ordtri3  4551  nsuceq0  4595  suctr  4598  ordnbtwn  4605  snnex  4646  uniuni  4649  iunpw  4692  oneqmin  4718  onuninsuci  4753  nlimsucg  4755  limomss  4783  nnlim  4791  peano5  4801  xpeq1  4825  xpeq2  4826  opthprc  4858  funopg  5418  dffv2  5728  dffo4  5817  elunirnALT  5932  f1oiso  6003  mpt2eq123  6065  ndmovg  6162  unielxp  6317  cnvf1o  6377  canth  6468  eusvobj2  6511  smoel  6551  smo11  6555  tz7.44-2  6594  oawordeulem  6726  oaordex  6730  omordi  6738  oneo  6753  oeordi  6759  oeoa  6769  oeoe  6771  nnmordi  6803  nnaordex  6810  omabs  6819  nnneo  6823  omsmolem  6825  elqsn0  6902  qsel  6912  mapsn  6984  undifixp  7027  boxriin  7033  boxcutc  7034  fineqvlem  7252  fineqv  7253  pssnn  7256  fissuni  7339  dffi2  7356  inficl  7358  dffi3  7364  wofib  7440  zfregcl  7488  suc11reg  7500  inf0  7502  inf3lem2  7510  inf3lem3  7511  infeq5i  7517  axinf2  7521  dfom3  7528  elom3  7529  noinfepOLD  7541  cantnfle  7552  oemapvali  7566  cantnflem1c  7569  cantnflem1  7571  en3lplem1  7596  en3lp  7598  tc2  7607  r1sdom  7626  rankwflemb  7645  rankval3b  7678  rankunb  7702  rankuni2b  7705  tcrank  7734  cardlim  7785  cardprclem  7792  infxpenlem  7821  alephnbtwn  7878  alephordi  7881  cardaleph  7896  alephfp  7915  alephval3  7917  aceq1  7924  aceq2  7926  dfac3  7928  dfac5lem2  7931  dfac5lem4  7933  dfac2  7937  kmlem2  7957  kmlem4  7959  coflim  8067  cfsmolem  8076  fin23lem30  8148  isf32lem2  8160  isf34lem4  8183  axdc2lem  8254  axdc3lem2  8257  axdc3lem4  8259  axdc4lem  8261  zorn2lem7  8308  axdclem  8325  brdom7disj  8335  brdom6disj  8336  axpowndlem3  8400  winainflem  8494  iswun  8505  eltskg  8551  inar1  8576  elgrug  8593  inaprc  8637  eltskm  8644  addnidpi  8704  indpi  8710  nqereu  8732  elnp  8790  elnpi  8791  genpnnp  8808  ltaddpr  8837  dfnn2  9938  dfnn3  9939  dfuzi  10285  uz11  10433  om2uzlti  11210  axdc4uz  11242  hashbclem  11621  hashf1lem2  11625  rpnnen2lem1  12734  rpnnen2lem2  12735  sadcp1  12887  ismre  13735  isacs  13796  mreclat  14533  issubm  14668  cycsubg  14888  isnsg  14889  subgacs  14895  nsgacs  14896  resghm  14942  ghmeql  14948  gsumzsplit  15449  pgpfac1lem1  15552  pgpfac1lem5  15557  pgpfac1  15558  issubrg  15788  islss  15931  lssacs  15963  lspsneq0  16008  lmhmeql  16051  lspdisjb  16118  lidl1el  16209  lidldvgen  16246  mplcoe1  16448  mplcoe2  16450  istopg  16884  fiinbas  16933  topbas  16953  ppttop  16987  pptbas  16988  epttop  16989  elcls  17053  clsndisj  17055  elcls3  17063  iscldtop  17075  neiptopnei  17112  restbas  17137  restntr  17161  pnfnei  17199  mnfnei  17200  cnpimaex  17235  lmcvg  17241  iscnp4  17242  cncnpi  17257  cnconst2  17262  cnprest  17268  cnprest2  17269  cnpdis  17272  lmss  17277  lmff  17280  cnt0  17325  ist1-3  17328  cnhaus  17333  isreg2  17356  dishaus  17361  ordthauslem  17362  cmpsublem  17377  cmpsub  17378  cmpcld  17380  hauscmplem  17384  uncon  17406  concompid  17408  concompcon  17409  concompss  17410  1stcfb  17422  1stcrest  17430  2ndcctbss  17432  2ndcomap  17435  dis2ndc  17437  1stcelcls  17438  llyeq  17447  nllyeq  17448  restnlly  17459  restlly  17460  islly2  17461  lly1stc  17473  dislly  17474  hauspwdom  17478  llycmpkgen2  17496  txbas  17513  eltx  17514  ptpjopn  17558  ptclsg  17561  dfac14lem  17563  txcnp  17566  ptcnplem  17567  ptcnp  17568  txlly  17582  pthaus  17584  txtube  17586  txhaus  17593  txlm  17594  tx1stc  17596  txkgen  17598  xkohaus  17599  xkopt  17601  xkococnlem  17605  tgqtop  17658  kqfvima  17676  kqt0lem  17682  isr0  17683  r0cld  17684  regr1lem  17685  kqreglem1  17687  kqreglem2  17688  reghmph  17739  fbssfi  17783  isfil  17793  filuni  17831  isufil  17849  isufil2  17854  uffix  17867  fixufil  17868  uffixfr  17869  uffixsn  17871  rnelfm  17899  flimopn  17921  flimrest  17929  flimcls  17931  flftg  17942  txflf  17952  fclsopni  17961  fclsrest  17970  fclscf  17971  fcfnei  17981  alexsublem  17989  alexsubALTlem3  17994  alexsubALT  17996  tmdgsum2  18040  symgtgp  18045  subgntr  18050  opnsubg  18051  tgpconcompeqg  18055  ghmcnp  18058  tgpt0  18062  divstgpopn  18063  tsmsi  18077  tsmssubm  18086  tsmssplit  18095  isust  18147  ustn0  18164  blss  18339  blssex  18340  neibl  18414  blcld  18418  metss  18421  methaus  18433  met1stc  18434  met2ndci  18435  metrest  18437  prdsxmslem2  18442  metcnp3  18453  dscopn  18485  idnghm  18641  qdensere  18668  tgioo  18691  tgqioo  18695  zdis  18711  xrge0tsms  18729  cnheibor  18844  lmmbr  19075  bcthlem4  19142  ovolicc2lem5  19277  dyadmbllem  19351  i1fd  19433  itg11  19443  itg2gt0  19512  itgeq1f  19523  bddmulibl  19590  ellimc2  19624  limcnlp  19625  ellimc3  19626  limcflf  19628  limciun  19641  lhop1lem  19757  ig1pdvds  19959  plycpn  20066  aannenlem2  20106  efopn  20409  xrlimcnp  20667  wilthlem2  20712  wilthlem3  20713  wilth  20714  usgra2edg  21261  usgraedg4  21265  nbgraf1olem1  21310  nbgraf1olem3  21312  nb3graprlem1  21319  nb3graprlem2  21320  uvtx01vtx  21360  uvtxnbgravtx  21363  constr1trl  21429  constr2trl  21439  vdgr1a  21518  vdusgra0nedg  21520  usgravd0nedg  21524  eupath2lem1  21540  lpni  21608  rngoueqz  21859  issh  22551  pjoc1  22777  h1dn0  22895  spansneleqi  22912  nonbooli  22994  pjch  23037  pjnel  23069  cdjreui  23776  rexunirn  23815  xrge0tsmsd  24045  tpr2rico  24107  lmxrge0  24134  indval  24200  issiga  24283  isrnsigaOLD  24284  isrnsiga  24285  ismbfm  24389  isanmbfm  24393  dya2icoseg  24414  dya2iocnrect  24418  ballotlem7  24565  erdszelem1  24649  kur14lem9  24672  cnllyscon  24704  cvmcov  24722  cvmsss2  24733  cvmcov2  24734  cvmseu  24735  cvmsiota  24736  cvmopnlem  24737  cvmliftlem15  24757  rtrclreclem.trans  24918  untelirr  24929  untsucf  24931  prodeq1f  25006  dfon2lem4  25159  dfon2lem7  25162  dfon2lem9  25164  soseq  25271  frrlem4  25301  frrlem5e  25306  frrlem11  25310  nodenselem8  25359  nocvxminlem  25361  nofulllem5  25377  dfiota3  25479  funpartlem  25498  funpartfun  25499  tfrqfree  25507  linethru  25794  hilbert1.1  25795  hilbert1.2  25796  rankelg  25816  elhf2  25823  fneint  26041  finlocfin  26063  locfindis  26069  comppfsc  26071  neibastop2lem  26073  cover2  26099  isbnd2  26176  prdstotbnd  26187  heibor1lem  26202  grpokerinj  26244  isidl  26308  1idl  26320  0rngo  26321  ispridl  26328  smprngopr  26346  isfldidl  26362  isdmn3  26368  elmzpcl  26467  diophren  26558  dford3lem2  26782  ttac  26791  pw2f1ocnv  26792  wepwsolem  26800  kelac1  26823  f1otrspeq  27052  pmtrval  27056  sdrgacs  27171  expgrowthi  27212  dvconstbi  27213  elunif  27348  fnchoice  27361  stoweidlem27  27437  stoweidlem35  27445  stoweidlem46  27456  stoweidlem52  27462  funressnfv  27654  fnbrafvb  27680  afvco2  27702  ndmaovg  27710  aovmpt4g  27727  vdn0frgrav2  27770  vdgn0frgrav2  27771  frgrancvvdeqlem4  27778  frgrancvvdeqlem7  27781  frgrancvvdeqlemA  27782  frgrancvvdeqlemC  27784  frgrawopreg1  27795  frgrawopreg2  27796  tratrb  27956  suctrALT2VD  28282  suctrALT2  28283  en3lplem1VD  28289  en3lpVD  28291  tratrbVD  28307  suctrALTcf  28368  suctrALTcfVD  28369  suctrALT3  28370  unisnALT  28372  bnj145  28425  bnj216  28430  bnj563  28442  bnj956  28478  bnj545  28597  bnj548  28599  bnj570  28607  bnj900  28631  bnj929  28638  bnj964  28645  bnj983  28653  bnj1001  28660  bnj1145  28693  bnj1398  28734  bnj1498  28761  lsateln0  29161  ispsubsp  29910  linepsubN  29917  elpcliN  30058  dvh3dim3N  31615  dochsnnz  31616  mapdindp3  31888
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753  ax-ext 2361
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-cleq 2373  df-clel 2376
  Copyright terms: Public domain W3C validator