MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqeltri Structured version   Visualization version   GIF version

Theorem eqeltri 2821
Description: Substitution of equal classes into membership relation. (Contributed by NM, 21-Jun-1993.)
Hypotheses
Ref Expression
eqeltri.1 𝐴 = 𝐵
eqeltri.2 𝐵𝐶
Assertion
Ref Expression
eqeltri 𝐴𝐶

Proof of Theorem eqeltri
StepHypRef Expression
1 eqeltri.2 . 2 𝐵𝐶
2 eqeltri.1 . . 3 𝐴 = 𝐵
32eleq1i 2816 . 2 (𝐴𝐶𝐵𝐶)
41, 3mpbir 230 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1533  wcel 2098
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-cleq 2717  df-clel 2802
This theorem is referenced by:  eqeltrri  2822  3eltr4i  2838  intab  4982  axrep6g  5294  unisn2  5313  inex2  5319  vpwex  5377  ord3ex  5387  zfpair  5421  vsnex  5431  opex  5466  otex  5467  uniopel  5518  elvvuni  5754  isarep2  6645  fvex  6909  fvexi  6910  riotaex  7379  ovexi  7453  tpex  7750  oprabex  7981  oprabrexex2  7983  mpoexw  8083  mptmpoopabbrd  8085  mptmpoopabbrdOLD  8086  tfrlem16  8414  1oex  8497  2oex  8498  1on  8499  1onOLD  8500  2on  8501  2onOLD  8502  3on  8505  4on  8506  2oexOLD  8508  oesuclem  8546  oecl  8558  o2p2e4  8562  nnecl  8634  1onnALT  8662  2onnALT  8664  3onn  8665  4onn  8666  mapsnf1o2  8913  sbthlem10  9117  imafi  9200  pwfi  9203  cnvfi  9205  fnfi  9206  nnunifi  9319  xpfiOLD  9344  prfi  9348  tpfi  9349  pwfiOLD  9373  fczfsuppd  9411  cantnfvalf  9690  oemapwe  9719  cantnffval2  9720  cnfcom3clem  9730  ssttrcl  9740  r1fin  9798  hta  9922  infxpenlem  10038  alephon  10094  alephfplem1  10129  dfac5lem4  10151  dfac5lem5  10152  kmlem10  10184  fin1a2lem10  10434  fin1a2lem12  10436  hsmexlem9  10450  axcc2lem  10461  domtriomlem  10467  axdc2lem  10473  axcclem  10482  brdom7disj  10556  brdom6disj  10557  iundom2g  10565  konigthlem  10593  canthwelem  10675  wunex2  10763  wunex3  10766  1nq  10953  1pr  11040  nrex1  11089  axcnex  11172  ax1cn  11174  pnfex  11299  mnfxr  11303  inelr  12235  cju  12241  nnexALT  12247  2nn  12318  2re  12319  2cn  12320  3nn  12324  3re  12325  3cn  12326  4nn  12328  4re  12329  4cn  12330  5nn  12331  5re  12332  5cn  12333  6nn  12334  6re  12335  6cn  12336  7nn  12337  7re  12338  7cn  12339  8nn  12340  8re  12341  8cn  12342  9nn  12343  9re  12344  9cn  12345  nn0ex  12511  zexALT  12611  nneo  12679  zeo  12681  deccl  12725  10re  12729  decnncl  12730  numnncl2  12733  decnncl2  12734  numsucc  12750  numma2c  12756  numadd  12757  numaddc  12758  nummul1c  12759  nummul2c  12760  decmul1  12774  qexALT  12981  xrex  13004  xnegex  13222  xnegcl  13227  ixxssxr  13371  om2uzuzi  13950  ltweuz  13962  axdc4uzlem  13984  seqex  14004  seqexw  14018  m1expcl2  14086  faccl  14278  facwordi  14284  faclbnd2  14286  bccl  14317  hashen1  14365  hashrabrsn  14367  hashunlei  14420  hashpw  14431  s1cli  14591  ccat2s1p1  14615  cats1un  14707  revs1  14751  cshwsexa  14810  cshwsexaOLD  14811  cats1cli  14844  cats1fvn  14845  crre  15097  remim  15100  climmpt  15551  sumex  15670  supcvg  15838  geo2lim  15857  prodex  15887  bpoly4  16039  ere  16069  eftlub  16089  efsep  16090  tan0  16131  ef01bndlem  16164  nn0o  16363  divalglem5  16377  divalglem9  16381  sadcf  16431  smupf  16456  crth  16750  phimullem  16751  pczpre  16819  pockthi  16879  prmreclem2  16889  igz  16906  0ramcl  16995  1259lem1  17103  1259lem2  17104  1259lem3  17105  1259lem4  17106  1259lem5  17107  1259prm  17108  2503lem1  17109  2503lem2  17110  2503lem3  17111  2503prm  17112  4001lem1  17113  4001lem2  17114  4001lem3  17115  4001lem4  17116  4001prm  17117  strle1  17130  ndxarg  17168  basendxnn  17193  basendxnnOLD  17194  plusgndxnn  17264  tsetndxnn  17338  plendxnn  17352  dsndxnn  17371  unifndxnn  17381  prdsbasex  17435  prdsds  17449  yonedalem3  18275  isposix  18320  isposixOLD  18321  plusffval  18609  issubmgm2  18666  efmnd1hash  18852  efmnd2hash  18854  smndex1bas  18866  smndex1sgrp  18868  smndex1mnd  18870  smndex1id  18871  smndex2dbas  18874  smndex2hbas  18876  grpsubfval  18948  mulgfval  19033  symg1hash  19356  symg2hash  19358  symgvalstruct  19363  symgvalstructOLD  19364  symgfisg  19435  psgnsn  19487  psgnprfval1  19489  odfval  19499  sylow2alem2  19585  efgsval2  19700  efgsp1  19704  pgpfaclem1  20050  dvdsrval  20312  isirred  20370  scaffval  20775  cnfldex  21299  xrsex  21327  pzriprnglem4  21427  pzriprnglem5  21428  pzriprnglem6  21429  pzriprng1ALT  21439  zlmlemOLD  21460  znle  21483  znidomb  21512  cnmsgnsubg  21526  refld  21568  ipffval  21597  psrbag0  22028  psrbagsn  22029  psr1baslem  22127  mat1dimbas  22418  mat1dimscm  22421  mat1f1o  22424  mat1rhmelval  22426  m2detleib  22577  pmatcoe1fsupp  22647  indistopon  22948  iccordt  23162  conncompid  23379  ptbasfi  23529  ptcmpfi  23761  ustfn  24150  ust0  24168  ustn0  24169  tmslem  24434  tmslemOLD  24435  nmfval  24541  tnglemOLD  24594  cnbl0  24734  cnopn  24747  remet  24750  re2ndc  24761  zcld  24773  icccmp  24785  xrge0gsumle  24793  xrge0tsms  24794  xmetdcn  24798  divcnOLD  24828  divcn  24830  expcn  24834  expcnOLD  24836  iiconn  24851  idcncf  24882  cnmpopc  24893  cnrehmeo  24922  cnrehmeoOLD  24923  cnheiborlem  24924  rellycmp  24927  bndth  24928  evth2  24930  cnrlmod  25114  cnrlvec  25115  cncmet  25294  ishl2  25342  ehleudis  25390  ehleudisval  25391  finiunmbl  25517  ioombl1lem4  25534  vitalilem4  25584  vitalilem5  25585  ismbf2d  25613  mbfimaopnlem  25628  mbfi1fseqlem6  25694  itgex  25744  bddmulibl  25812  ditgex  25825  recnperf  25878  dvcnvrelem2  25995  ftc1  26021  mdegcl  26049  plyeq0lem  26189  aaliou3lem4  26326  dvradcnv  26402  sincn  26426  coscn  26427  tanabsge  26486  circsubm  26532  reloggim  26578  logcn  26626  dvloglem  26627  logdmopn  26628  dvlog2  26632  2irrexpq  26710  cxpcn  26724  cxpcnOLD  26725  cxpcn3  26728  resqrtcn  26729  2logb9irrALT  26775  2irrexpqALT  26777  atanrecl  26888  atan1  26905  atansopn  26909  birthdaylem1  26928  birthday  26931  emcllem4  26976  emcllem6  26978  lgamgulmlem6  27011  basellem6  27063  ppiublem1  27180  bposlem6  27267  bposlem8  27269  lgslem4  27278  lgsdir2lem2  27304  selberglem1  27523  selberglem3  27525  selberg  27526  selbergs  27552  qdrng  27598  0sno  27805  1sno  27806  lrrecse  27905  precsexlem11  28165  seqsex  28208  nnsex  28240  n0sbday  28269  n0subs  28275  n0p1nns  28276  zsex  28279  edgfndxnn  28875  structvtxvallem  28905  usgrexmpllem  29145  usgrexmpl  29148  uhgrspan1  29188  upgrres  29191  umgrres  29192  usgrres  29193  upgrres1  29198  umgrres1  29199  usgrres1  29200  fusgrfis  29215  cusgrres  29334  vtxdlfgrval  29371  vtxdusgr0edgnelALT  29382  umgr2v2e  29411  vtxdginducedm1lem1  29425  vtxdginducedm1fi  29430  finsumvtxdg2ssteplem4  29434  pthdlem1  29652  crctcshlem3  29702  2wlkd  29819  2wlkond  29820  2trlond  29822  2pthd  29823  2pthond  29825  umgr2adedgwlkonALT  29830  0pth  30007  wlk2v2e  30039  3wlkd  30052  3trlond  30055  3pthd  30056  3pthond  30057  3spthond  30059  eupthvdres  30117  eulerpathpr  30122  konigsbergumgr  30133  konigsberglem5  30138  konigsberg  30139  ex-lcm  30340  isvciOLD  30462  isnvi  30495  blocni  30687  hmoval  30692  cncph  30701  ipasslem7  30718  siilem2  30734  normlem2  30993  normlem3  30994  normlem6  30997  h0elch  31137  hhssabloilem  31143  hhsssh  31151  spansnji  31528  nonbooli  31533  3oalem5  31548  3oalem6  31549  3oai  31550  mayetes3i  31611  nmcexi  31908  nmbdfnlb  31932  rnelshi  31941  cnlnadjlem5  31953  pjbdlni  32031  golem2  32154  goeqi  32155  dp2clq  32689  rpdp2cl  32690  rpdp2cl2  32691  dpmul100  32705  rpdpcl  32711  xrge0tsmsd  32861  pmtrto1cl  32912  psgnfzto1stlem  32913  fzto1st  32916  psgnfzto1st  32918  nn0omnd  33156  xrge0slmod  33159  qusima  33220  prmidl0  33262  fply1  33371  ply1degltdimlem  33451  ccfldextdgrr  33491  algextdeglem8  33523  circtopn  33569  circcn  33570  zarcmplem  33613  tpr2tp  33636  tpr2rico  33644  ordtprsval  33650  ordtprsuni  33651  ordtrestNEW  33653  ordtrest2NEWlem  33654  ordtrest2NEW  33655  ordtconnlem1  33656  mndpluscn  33658  xrge0pluscn  33672  xrge0mulc1cn  33673  xrge0haus  33676  lmlimxrge0  33680  lmxrge0  33684  qqhcn  33723  qqhucn  33724  esumex  33779  esumcst  33813  hasheuni  33835  esumcvg  33836  prsiga  33881  brsiga  33933  mbfmcnt  34019  sxbrsigalem3  34023  dya2iocuni  34034  dya2iocucvr  34035  sxbrsigalem1  34036  sxbrsiga  34041  eulerpartlemt  34122  fibp1  34152  coinflipprob  34230  coinfliprv  34233  ccatmulgnn0dir  34305  signswplusg  34318  hgt750lem2  34415  hgt750leme  34421  bnj105  34486  bnj918  34528  bnj95  34626  bnj852  34683  bnj865  34685  subfacp1lem1  34920  subfacp1lem3  34923  subfacp1lem5  34925  subfacp1lem6  34926  kur14lem7  34953  iisconn  34993  iillysconn  34994  cvmliftlem5  35030  cvmliftlem8  35033  cvmliftlem10  35035  cvmlift2lem9  35052  satfv0  35099  goalrlem  35137  goalr  35138  satffunlem2lem2  35147  circum  35409  iexpire  35460  altopex  35687  colinearex  35787  ssoninhaus  36063  cnndvlem2  36144  bj-prex  36650  bj-prfromadj  36655  bj-pinftyccb  36831  taupi  36933  isbasisrelowl  36968  relowlpssretop  36974  poimirlem29  37253  poimirlem30  37254  poimirlem31  37255  dvasin  37308  dvacos  37309  areacirc  37317  upixp  37333  fdc  37349  lmclim2  37362  cncfres  37369  heibor1lem  37413  rrnval  37431  rrnmet  37433  reheibor  37443  isdrngo2  37562  isrngohom  37569  idlval  37617  isidl  37618  igenval  37665  scottexf  37772  cnvepresex  37936  renegclALT  38565  ldualfvadd  38730  cmtfvalN  38812  cvrfval  38870  cdleme31fv  39993  cdlemk40  40520  cdlemk56  40574  dibopelvalN  40746  dibopelval2  40748  dibelval3  40750  diblsmopel  40774  cdlemn11a  40810  dihopelvalcpre  40851  dihpN  40939  hlhilsca  41538  hlhilip  41555  3factsumint1  41624  lcmineqlem23  41654  aks4d1p1p6  41676  aks4d1p1p5  41678  aks6d1c6isolem2  41778  itrere  42014  sn-0tie0  42129  sn-itrere  42156  sn-retire  42157  prjspval  42162  flt4lem5e  42215  sn-isghm  42232  acos1half  42233  mapfzcons2  42281  jm2.23  42559  jm2.27dlem2  42573  jm2.27dlem4  42575  rmydioph  42577  rmxdioph  42579  expdiophlem2  42585  expdioph  42586  aomclem6  42625  pwslnmlem0  42657  frlmpwfi  42664  mncn0  42705  aaitgo  42728  arearect  42785  areaquad  42786  omcl3g  42905  comptiunov2i  43278  frege110  43545  frege133  43568  scottex2  43824  radcnvrat  43893  uzmptshftfval  43925  dvradcnv2  43926  binomcxplemdvbinom  43932  binomcxplemcvg  43933  binomcxplemnotnn0  43935  rfcnpre1  44523  fcnre  44529  refsumcn  44534  refsum2cnlem1  44541  unirnmapsn  44726  infxrpnf  44966  iocopn  45043  icoopn  45048  mccl  45124  clim1fr1  45127  islptre  45145  sumnnodd  45156  lptre2pt  45166  limclner  45177  limclr  45181  expfac  45183  0cnf  45403  icccncfext  45413  ioodvbdlimc1lem2  45458  ioodvbdlimc2lem  45460  itgsin0pilem1  45476  iblempty  45491  itgvol0  45494  stoweidlem47  45573  stoweidlem53  45579  stoweidlem57  45583  stoweidlem59  45585  wallispilem3  45593  wallispilem4  45594  wallispilem5  45595  wallispi  45596  stirlinglem1  45600  stirlinglem8  45607  stirlinglem12  45611  stirlinglem13  45612  stirlinglem14  45613  stirlinglem15  45614  dirkerper  45622  dirkercncflem2  45630  fourierdlem16  45649  fourierdlem21  45654  fourierdlem22  45655  fourierdlem36  45669  fourierdlem42  45675  fourierdlem71  45703  fourierdlem83  45715  fourierdlem102  45734  fourierdlem103  45735  fourierdlem104  45736  fourierdlem111  45743  fourierdlem112  45744  fourierdlem114  45746  sqwvfoura  45754  sqwvfourb  45755  fourierswlem  45756  fouriersw  45757  etransclem48  45808  salexct3  45868  salgencntex  45869  salgensscntex  45870  iooborel  45877  bor1sal  45881  gsumge0cl  45897  sge0tsms  45906  sge0isum  45953  nnfoctbdjlem  45981  isomenndlem  46056  mbfresmf  46265  incsmflem  46267  incsmf  46268  smfmbfcex  46286  decsmflem  46292  decsmf  46293  smflimlem1  46297  smfpimbor1lem2  46325  smf2id  46327  smfco  46328  smfpimcclem  46333  tworepnotupword  46410  sprsymrelfolem1  46969  sprbisymrel  46976  fmtno0prm  47035  fmtno1prm  47036  fmtno2prm  47037  fmtno3prm  47039  fmtno4prm  47052  m2prm  47068  m3prm  47069  m5prm  47075  m7prm  47077  lighneallem4a  47085  0evenALTV  47165  1oddALTV  47167  2evenALTV  47169  6even  47188  7odd  47189  8even  47190  9gbo  47251  opstrgric  47378  ushggricedg  47379  uspgrex  47398  lmod1zrnlvec  47748  zlmodzxzldeplem1  47754  zlmodzxzldeplem3  47756  zlmodzxzldeplem4  47757  zlmodzxzldep  47758  ldepsnlinclem1  47759  ldepsnlinclem2  47760  blennn0elnn  47836  nn0sumshdiglemA  47878  nn0sumshdiglemB  47879  itcovalpclem2  47930  itcovalt2lem2  47935  ackval42  47955  rrx2line  47999  rrx2linesl  48002  spheres  48005  2sphere  48008  2sphere0  48009  line2x  48013  line2y  48014  functhinclem1  48233  prsthinc  48246
  Copyright terms: Public domain W3C validator