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

Theorem eleq2 2504
Description: Equality implies equivalence of membership. (Contributed by NM, 26-May-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 2437 . . . . . 6  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
21biimpi 194 . . . . 5  |-  ( A  =  B  ->  A. x
( x  e.  A  <->  x  e.  B ) )
3219.21bi 1804 . . . 4  |-  ( A  =  B  ->  (
x  e.  A  <->  x  e.  B ) )
43anbi2d 703 . . 3  |-  ( A  =  B  ->  (
( x  =  C  /\  x  e.  A
)  <->  ( x  =  C  /\  x  e.  B ) ) )
54exbidv 1680 . 2  |-  ( A  =  B  ->  ( E. x ( x  =  C  /\  x  e.  A )  <->  E. x
( x  =  C  /\  x  e.  B
) ) )
6 df-clel 2439 . 2  |-  ( C  e.  A  <->  E. x
( x  =  C  /\  x  e.  A
) )
7 df-clel 2439 . 2  |-  ( C  e.  B  <->  E. x
( x  =  C  /\  x  e.  B
) )
85, 6, 73bitr4g 288 1  |-  ( A  =  B  ->  ( C  e.  A  <->  C  e.  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369   A.wal 1367    = wceq 1369   E.wex 1586    e. wcel 1756
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-cleq 2436  df-clel 2439
This theorem is referenced by:  eleq12  2505  eleq2i  2507  eleq2d  2510  nelneq2  2545  dvelimdc  2611  nelne1  2722  neleq2  2731  raleqf  2934  rexeqf  2935  reueq1f  2936  rmoeq1f  2937  rabeqf  2986  clel3g  3118  clel4  3120  sbcbi2  3258  sbcel2gv  3274  csbeq2  3313  difeq2  3489  uneq1  3524  ineq1  3566  unineq  3621  n0i  3663  sbnfc2  3727  disjel  3746  elif  3850  exsnrex  3935  sneqr  4061  preqr1  4067  preq12b  4069  prel12  4070  elunii  4117  eluniab  4123  ssuni  4134  elinti  4158  elintab  4160  intss1  4164  intmin  4169  intab  4179  iineq2  4209  dfiin2g  4224  breq  4315  zfrepclf  4430  axsep2  4435  zfauscl  4436  sseliALT  4444  inuni  4475  pwne0  4483  elALT  4556  rext  4561  intid  4571  opth1  4586  opthwiener  4614  ordtri1  4773  ordtri3  4776  nsuceq0  4820  suctr  4823  ordnbtwn  4830  xpeq1  4875  xpeq2  4876  opthprc  4907  funopg  5471  dffv2  5785  dffo4  5880  fnsnb  5919  elunirn  5989  f1oiso  6063  canth  6070  eusvobj2  6105  mpt2eq123  6166  ndmovg  6267  snnex  6403  uniuni  6406  iunpw  6411  oneqmin  6437  onuninsuci  6472  nlimsucg  6474  limomss  6502  nnlim  6510  peano5  6520  unielxp  6633  cnvf1o  6692  smoel  6842  smo11  6846  tz7.44-2  6884  oawordeulem  7014  oaordex  7018  omordi  7026  oneo  7041  oeordi  7047  oeoa  7057  oeoe  7059  nnmordi  7091  nnaordex  7098  omabs  7107  nnneo  7111  omsmolem  7113  elqsn0  7190  qsel  7200  mapsn  7275  undifixp  7320  boxriin  7326  boxcutc  7327  fineqvlem  7548  fineqv  7549  pssnn  7552  fissuni  7637  dffi2  7694  inficl  7696  dffi3  7702  wofib  7780  zfregcl  7830  en3lplem1  7841  en3lp  7843  suc11reg  7846  inf0  7848  inf3lem2  7856  inf3lem3  7857  infeq5i  7863  axinf2  7867  dfom3  7874  elom3  7875  noinfepOLD  7887  cantnfle  7900  oemapvali  7913  cantnflem1c  7916  cantnflem1  7918  cantnfleOLD  7930  cantnflem1cOLD  7939  cantnflem1OLD  7941  tc2  7983  r1sdom  8002  rankwflemb  8021  rankval3b  8054  rankunb  8078  rankuni2b  8081  tcrank  8112  cardlim  8163  cardprclem  8170  infxpenlem  8201  alephnbtwn  8262  alephordi  8265  cardaleph  8280  alephfp  8299  alephval3  8301  aceq1  8308  aceq2  8310  dfac3  8312  dfac5lem2  8315  dfac5lem4  8317  dfac2  8321  kmlem2  8341  kmlem4  8343  coflim  8451  cfsmolem  8460  fin23lem30  8532  isf32lem2  8544  isf34lem4  8567  axdc2lem  8638  axdc3lem2  8641  axdc3lem4  8643  axdc4lem  8645  zorn2lem7  8692  axdclem  8709  brdom7disj  8719  brdom6disj  8720  axpowndlem3  8785  axpowndlem3OLD  8786  winainflem  8881  iswun  8892  eltskg  8938  inar1  8963  elgrug  8980  inaprc  9024  eltskm  9031  addnidpi  9091  indpi  9097  nqereu  9119  elnp  9177  elnpi  9178  genpnnp  9195  ltaddpr  9224  dfnn2  10356  dfnn3  10357  dfuzi  10753  uz11  10904  om2uzlti  11794  axdc4uz  11826  hash2prd  12202  hashbclem  12226  hashf1lem2  12230  wrdsymb0  12280  lsw0  12288  rpnnen2lem1  13518  rpnnen2lem2  13519  sadcp1  13672  ismre  14549  isacs  14610  clatl  15307  mreclatBAD  15378  issubm  15496  cycsubg  15730  isnsg  15731  subgacs  15737  nsgacs  15738  resghm  15784  ghmeql  15790  gsmsymgreq  15958  f1otrspeq  15974  pmtrval  15978  pmtrdifellem4  16006  pmtrprfval  16014  gsumzsplit  16439  gsumzsplitOLD  16440  pgpfac1lem1  16597  pgpfac1lem5  16602  pgpfac1  16603  issubrg  16887  islss  17038  lssacs  17070  lspsneq0  17115  lmhmeql  17158  lspdisjb  17229  lidl1el  17322  lidldvgen  17359  mplcoe1  17566  mplcoe5  17570  mplcoe2OLD  17572  islindf4  18289  mdetunilem9  18448  maducoeval2  18468  madugsum  18471  istopg  18530  fiinbas  18579  topbas  18599  ppttop  18633  pptbas  18634  epttop  18635  elcls  18699  clsndisj  18701  elcls3  18709  iscldtop  18721  neiptopnei  18758  restbas  18784  restntr  18808  pnfnei  18846  mnfnei  18847  cnpimaex  18882  lmcvg  18888  iscnp4  18889  cncnpi  18904  cnconst2  18909  cnprest  18915  cnprest2  18916  cnpdis  18919  lmss  18924  lmff  18927  cnt0  18972  ist1-3  18975  cnhaus  18980  isreg2  19003  dishaus  19008  ordthauslem  19009  cmpsublem  19024  cmpsub  19025  cmpcld  19027  hauscmplem  19031  bwthOLD  19036  uncon  19055  concompid  19057  concompcon  19058  concompss  19059  1stcfb  19071  1stcrest  19079  2ndcctbss  19081  2ndcomap  19084  dis2ndc  19086  1stcelcls  19087  llyeq  19096  nllyeq  19097  restnlly  19108  restlly  19109  islly2  19110  lly1stc  19122  dislly  19123  hauspwdom  19127  llycmpkgen2  19145  txbas  19162  eltx  19163  ptpjopn  19207  ptclsg  19210  dfac14lem  19212  txcnp  19215  ptcnplem  19216  ptcnp  19217  txlly  19231  pthaus  19233  txtube  19235  txhaus  19242  txlm  19243  tx1stc  19245  txkgen  19247  xkohaus  19248  xkopt  19250  xkococnlem  19254  tgqtop  19307  kqfvima  19325  kqt0lem  19331  isr0  19332  r0cld  19333  regr1lem  19334  kqreglem1  19336  kqreglem2  19337  reghmph  19388  fbssfi  19432  isfil  19442  filuni  19480  isufil  19498  isufil2  19503  uffix  19516  fixufil  19517  uffixfr  19518  uffixsn  19520  rnelfm  19548  flimopn  19570  flimrest  19578  flimcls  19580  flftg  19591  txflf  19601  fclsopni  19610  fclsrest  19619  fclscf  19620  fcfnei  19630  alexsublem  19638  alexsubALTlem3  19643  alexsubALT  19645  tmdgsum2  19689  symgtgp  19694  subgntr  19699  opnsubg  19700  tgpconcompeqg  19704  ghmcnp  19707  tgpt0  19711  divstgpopn  19712  tsmsi  19726  tsmssubm  19738  tsmssplit  19748  isust  19800  ustn0  19817  blssps  20021  blss  20022  blssexps  20023  blssex  20024  neibl  20098  blcld  20102  metss  20105  methaus  20117  met1stc  20118  met2ndci  20119  metrest  20121  prdsxmslem2  20126  metcnp3  20137  dscopn  20188  idnghm  20344  qdensere  20371  tgioo  20395  tgqioo  20399  zdis  20415  xrge0tsms  20433  cnheibor  20549  lmmbr  20791  bcthlem4  20860  ovolicc2lem5  21026  dyadmbllem  21101  i1fd  21181  itg11  21191  itg2gt0  21260  itgeq1f  21271  bddmulibl  21338  ellimc2  21374  limcnlp  21375  ellimc3  21376  limcflf  21378  limciun  21391  lhop1lem  21507  ig1pdvds  21670  plycpn  21777  aannenlem2  21817  efopn  22125  xrlimcnp  22384  wilthlem2  22429  wilthlem3  22430  wilth  22431  tghilbert1_1  23065  tghilbert1_2  23066  colline  23074  usgra2edg  23323  usgraedg4  23327  nbgraf1olem1  23372  nbgraf1olem3  23374  nb3graprlem1  23381  nb3graprlem2  23382  uvtx01vtx  23422  uvtxnbgravtx  23425  2trllemF  23470  wlkntrl  23483  constr1trl  23509  vdgr1a  23598  vdusgra0nedg  23600  usgravd0nedg  23604  eupath2lem1  23620  lpni  23688  rngoueqz  23939  issh  24632  pjoc1  24859  h1dn0  24977  spansneleqi  24994  nonbooli  25076  pjch  25119  pjnel  25151  cdjreui  25858  rexunirn  25897  rabsnel  25909  opabdm  25965  opabrn  25966  fpwrelmapffslem  26054  fpwrelmap  26055  xrge0tsmsd  26275  tpr2rico  26364  lmxrge0  26404  indval  26492  issiga  26576  isrnsigaOLD  26577  isrnsiga  26578  ddeval1  26672  ddeval0  26673  ddemeas  26674  ismbfm  26689  isanmbfm  26693  dya2icoseg  26714  dya2iocnrect  26718  ballotlem7  26940  erdszelem1  27101  kur14lem9  27124  cnllyscon  27156  cvmcov  27174  cvmsss2  27185  cvmcov2  27186  cvmseu  27187  cvmsiota  27188  cvmopnlem  27189  cvmliftlem15  27209  rtrclreclem.trans  27370  untelirr  27381  untsucf  27383  prodeq1f  27443  dfon2lem4  27621  dfon2lem7  27624  dfon2lem9  27626  soseq  27737  frrlem4  27793  frrlem5e  27798  frrlem11  27802  nodenselem8  27851  nocvxminlem  27853  nofulllem5  27869  dfiota3  27976  funpartlem  27995  funpartfun  27996  tfrqfree  28004  linethru  28206  hilbert1.1  28207  hilbert1.2  28208  rankelg  28228  elhf2  28235  fin2so  28442  heicant  28452  mblfinlem1  28454  ftc1anc  28501  ftc2nc  28502  fneint  28575  finlocfin  28597  locfindis  28603  comppfsc  28605  neibastop2lem  28607  cover2  28633  isbnd2  28708  prdstotbnd  28719  heibor1lem  28734  grpokerinj  28776  isidl  28840  1idl  28852  0rngo  28853  ispridl  28860  smprngopr  28878  isfldidl  28894  isdmn3  28900  iuneq2f  28993  mpt2bi123f  29001  iineq12f  29003  mptbi12f  29005  elmzpcl  29088  diophren  29178  dford3lem2  29402  ttac  29411  pw2f1ocnv  29412  wepwsolem  29420  kelac1  29442  sdrgacs  29584  expgrowthi  29633  dvconstbi  29634  elunif  29764  fnchoice  29777  stoweidlem27  29848  stoweidlem35  29856  stoweidlem46  29867  stoweidlem52  29873  funressnfv  30060  fnbrafvb  30086  afvco2  30108  ndmaovg  30116  aovmpt4g  30133  fzoopth  30239  elfzonlteqm1  30251  hash2prv  30252  hashrabsn1  30259  eleclclwwlkn  30533  vdn0frgrav2  30642  vdgn0frgrav2  30643  frgrancvvdeqlem4  30652  frgrancvvdeqlem7  30655  frgrancvvdeqlemA  30656  frgrancvvdeqlemC  30658  frgrawopreg1  30669  frgrawopreg2  30670  0rng01eq  30806  m1detdiag  30931  ldepspr  31004  tratrb  31338  suctrALT2VD  31668  suctrALT2  31669  en3lplem1VD  31675  en3lpVD  31677  tratrbVD  31693  suctrALTcf  31754  suctrALTcfVD  31755  suctrALT3  31756  unisnALT  31758  bnj145OLD  31814  bnj216  31819  bnj563  31831  bnj956  31866  bnj545  31984  bnj548  31986  bnj570  31994  bnj900  32018  bnj929  32025  bnj964  32032  bnj983  32040  bnj1001  32047  bnj1145  32080  bnj1398  32121  bnj1498  32148  bj-rabeqd  32519  bj-cleq  32550  bj-snsetex  32552  bj-elopg  32618  lsateln0  32736  ispsubsp  33485  linepsubN  33492  elpcliN  33633  dvh3dim3N  35190  dochsnnz  35191  mapdindp3  35463
  Copyright terms: Public domain W3C validator