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

Theorem eleqtrrdi 2922
Description: A membership and equality inference. (Contributed by NM, 24-Apr-2005.)
Hypotheses
Ref Expression
eleqtrrdi.1 (𝜑𝐴𝐵)
eleqtrrdi.2 𝐶 = 𝐵
Assertion
Ref Expression
eleqtrrdi (𝜑𝐴𝐶)

Proof of Theorem eleqtrrdi
StepHypRef Expression
1 eleqtrrdi.1 . 2 (𝜑𝐴𝐵)
2 eleqtrrdi.2 . . 3 𝐶 = 𝐵
32eqcomi 2829 . 2 𝐵 = 𝐶
41, 3eleqtrdi 2921 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1537  wcel 2114
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2792
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2813  df-clel 2891
This theorem is referenced by:  3eltr4g  2928  brelrng  5783  elabrex  6975  fliftel1  7036  ovidig  7265  unielxp  7701  tfrlem11  7998  rdglim  8036  seqomlem4  8063  2oconcl  8102  ecopqsi  8328  erov  8368  eroprf  8369  sbthlem2  8602  dffi3  8869  ixpiunwdom  9029  cantnfcl  9104  r1lim  9175  rankwflemb  9196  pwwf  9210  unwf  9213  rankwflem  9218  uniwf  9222  rankpwi  9226  rankr1g  9235  r1pw  9248  r1rankid  9262  rankuni  9266  djulcl  9313  djurcl  9314  inlresf  9317  inrresf  9319  djuun  9329  cardlim  9375  infxpenlem  9413  alephfp  9508  cfsmolem  9666  alephsing  9672  hsmexlem4  9825  axdc3lem2  9847  numth3  9866  iunfo  9935  konigthlem  9964  iunctb  9970  canthwelem  10046  canthwe  10047  r1limwun  10132  inar1  10171  inatsk  10174  gruina  10214  grur1  10216  tskmval  10235  tskmcl  10237  pinq  10323  dmrecnq  10364  addclsr  10479  mulclsr  10480  axaddf  10541  axmulf  10542  peano2nn  11624  uztrn2  12237  eluz2nn  12259  peano2uzs  12277  uzsupss  12315  uzsup  13211  uzrdgfni  13306  uzrdgsuci  13308  fsuppmapnn0fiub  13339  seqf  13372  ser0  13403  bcm1k  13656  bcp1nk  13658  bcpasc  13662  hashprdifel  13740  fz1isolem  13800  pr2pwpr  13818  ccats1val2  13959  rexuzre  14688  limsupgre  14814  climconst  14876  rlimclim1  14878  climrlim2  14880  clim2ser  14987  clim2ser2  14988  iserex  14989  isermulc2  14990  iserle  14992  isercolllem3  14999  isercoll2  15001  climsup  15002  iseraltlem2  15015  iseraltlem3  15016  zsum  15051  isumclim3  15090  isumadd  15098  fsump1i  15100  iserabs  15146  cvgcmp  15147  cvgcmpub  15148  cvgcmpce  15149  abscvgcvg  15150  isumshft  15170  isumsplit  15171  isum1p  15172  isumrpcl  15174  isumsup2  15177  climcndslem1  15180  cvgrat  15215  clim2prod  15220  clim2div  15221  prodf1  15223  ntrivcvgn0  15230  ntrivcvgtail  15232  fprodntriv  15272  fprodabs  15304  fprodeq0  15305  iprodclim3  15330  iprodmul  15333  ef0lem  15408  fprodefsum  15424  rpnnen2lem3  15545  dvdsflip  15643  fzo0dvdseq  15649  bitsinv1  15765  smupval  15811  smueqlem  15813  seq1st  15889  algr0  15890  prmind2  16003  crth  16089  eulerthlem2  16093  prmdiv  16096  pockthlem  16215  pockthg  16216  unbenlem  16218  prmunb  16224  prmgaplem7  16367  strfv2d  16504  imasvscaval  16786  oppccatid  16964  epii  16988  fthepi  17173  funcestrcsetclem3  17367  funcsetcestrclem3  17381  yon12  17490  yon2  17491  yonedalem4c  17502  yonedalem22  17503  yonedalem3b  17504  yonedainv  17506  acsmapd  17763  mgm2nsgrplem1  18058  mgm2nsgrplem2  18059  mgm2nsgrplem3  18060  sgrp2nmndlem1  18063  sgrp2rid2  18066  cntrsubgnsg  18446  symgpssefmnd  18499  pmtrrn  18560  gexcl3  18687  efgi  18820  efgi2  18826  efgs1b  18837  efgredlemg  18843  efgredlemd  18845  frgpnabllem1  18968  cycsubgcyg  18996  gsumzaddlem  19016  dprdwd  19108  dprd2da  19139  lsppratlem3  19893  lsppratlem4  19894  lbsextlem2  19903  lidl0  19964  lidl1  19965  mplsubrglem  20191  mpfconst  20286  mpfproj  20287  mpfind  20292  pf1const  20481  pf1id  20482  mpfpf1  20486  pf1mpf  20487  domnchr  20651  znf1o  20670  madetsumid  21042  slesolex  21263  pmatcoe1fsupp  21281  mat2pmatbas0  21307  pmatcollpw  21361  pm2mpf1  21379  isclo  21667  indiscld  21671  restntr  21762  ordtbaslem  21768  ordtbas2  21771  lmconst  21841  lmss  21878  conncompid  22011  2ndcomap  22038  locfincmp  22106  comppfsc  22112  xkouni  22179  txcls  22184  ptclsg  22195  uptx  22205  txindis  22214  tx1stc  22230  cnmpt1res  22256  tgqtop  22292  uffix  22501  cnpflf2  22580  ptcmplem2  22633  ptcmplem4  22635  tgpconncomp  22693  tsmsfbas  22708  fmucnd  22873  prdsxmetlem  22950  imasdsf1olem  22955  prdsbl  23073  blcvx  23378  xrsmopn  23392  xrge0tsms  23414  metdcn2  23419  expcncf  23506  cnmpopc  23508  icchmeo  23521  iccpnfhmeo  23525  cnheibor  23535  evth  23539  evth2  23540  lebnumlem2  23542  lebnumii  23546  reparphti  23577  cfilfcls  23853  minveclem2  24005  minveclem3  24008  minveclem4  24011  ovoliunlem1  24081  ovolicc1  24095  iundisj  24127  volsup  24135  uniioombllem3  24164  vitalilem2  24188  vitalilem3  24189  mbfsup  24243  mbfinf  24244  mbflimsup  24245  itg2monolem1  24329  limcflflem  24458  limccnp  24469  limccnp2  24470  dvidlem  24493  dvn2bss  24508  cpnres  24515  dvcobr  24524  dvrec  24533  c1liplem1  24574  dvcnvrelem2  24596  dvfsumrlimf  24603  dvfsumlem1  24604  dvfsumlem2  24605  dvfsumlem3  24606  dvfsumlem4  24607  dvfsumrlim  24609  dvfsum2  24612  coeeulem  24796  coeid3  24812  plycn  24833  dvntaylp  24941  taylthlem1  24943  taylthlem2  24944  ulm2  24955  ulmshftlem  24959  ulmshft  24960  ulm0  24961  ulmcn  24969  ulmdvlem3  24972  ulmdv  24973  mtest  24974  mtestbdd  24975  dvradcnv  24991  psercn2  24993  psercn  24996  pserdv  24999  abelth  25011  efif1olem2  25110  efif1olem4  25112  efifo  25114  eff1olem  25115  logcn  25213  dvloglem  25214  cxpcn3  25312  resqrtcn  25313  sqrtcn  25314  logbleb  25344  logblt  25345  asinneg  25447  atanlogsub  25477  atanbnd  25487  ressatans  25495  leibpilem2  25502  xrlimcnp  25529  efrlim  25530  scvxcvx  25546  ppiub  25763  chtub  25771  logexprlim  25784  lgseisenlem1  25934  rplogsumlem1  26043  rplogsumlem2  26044  dchrisumlem2  26049  dchrisum0flb  26069  logdivbnd  26115  pntlem3  26168  tgcgr4  26300  ltgov  26366  f1otrg  26640  eengtrkg  26755  iedgedg  26818  ushgredgedgloop  26996  subgruhgredgd  27049  uvtxupgrres  27173  umgr2v2evd2  27292  edginwlk  27399  wlk1walk  27403  crctcshwlkn0lem6  27576  wlkiswwlks1  27628  minvecolem1  28632  minvecolem2  28633  minvecolem4  28638  htthlem  28675  5oalem2  29413  3oalem2  29421  iundisjf  30322  fmptco1f1o  30361  xppreima  30377  xppreima2  30378  dfcnv2  30405  xrge0tsmsd  30696  odpmco  30734  pmtrcnelor  30739  pmtrto1cl  30745  psgnfzto1stlem  30746  fzto1stfv1  30747  fzto1st  30749  fzto1stinvn  30750  psgnfzto1st  30751  tocycf  30763  cycpmco2lem7  30778  cycpmco2  30779  cycpmrn  30789  cyc3evpm  30796  cyc3genpmlem  30797  cycpmgcl  30799  cyc3conja  30803  rhmopp  30896  fply1  30935  ssmxidllem  30985  smatlem  31069  smatcl  31074  tpr2rico  31159  xrmulc1cn  31177  xrge0mulc1cn  31188  esumpfinvallem  31337  ldgenpisyslem1  31426  dynkin  31430  brfae  31511  sxbrsigalem3  31534  dya2icoseg2  31540  omsmeas  31585  sibfof  31602  sseqmw  31653  sseqf  31654  sseqp1  31657  fiblem  31660  fibp1  31663  probfinmeasbALTV  31691  repr0  31886  reprpmtf1o  31901  hgt750lemg  31929  bnj1379  32106  srcmpltd  32350  subfacp1lem5  32435  subfacp1lem6  32436  cvxpconn  32493  cvxsconn  32494  cvmliftlem6  32541  cvmliftlem8  32543  cvmliftlem10  32545  cvmlift2lem6  32559  cvmlift2lem11  32564  cvmlift2lem12  32565  2goelgoanfmla1  32675  prv1n  32682  msubff  32781  msubco  32782  elmsta  32799  msubff1  32807  mvhf  32809  msubvrs  32811  iprodefisumlem  32976  filnetlem3  33732  knoppcnlem10  33845  knoppcnlem11  33846  icoreunrn  34653  icoreelrn  34655  ralssiun  34701  poimirlem3  34932  poimirlem16  34945  poimirlem17  34946  poimirlem19  34948  poimirlem30  34959  dvasin  35013  cover2  35024  upixp  35039  sdclem1  35053  fdc  35055  caushft  35071  ismtyres  35118  rrncmslem  35142  isfld2  35315  osumcllem10N  37133  pexmidlem7N  37144  dihglblem2N  38462  lcfrvalsnN  38709  lcfrlem5  38714  lcfrlem6  38715  lcfrlem27  38737  lcfrlem37  38747  prjspvs  39393  0prjspnrel  39402  monotuz  39671  expdiophlem1  39751  kelac2  39798  grurankcld  40720  dvgrat  40795  nzss  40800  uzmptshftfval  40829  binomcxplemnotnn0  40839  refsumcn  41438  rfcnpre2  41439  rfcnpre3  41441  rfcnpre4  41442  elabrexg  41454  disjf1o  41602  unirnmap  41621  unirnmapsn  41627  ssmapsn  41629  mptssid  41661  allbutfi  41815  eluzd  41832  uzidd2  41840  ressiocsup  41978  ressioosup  41979  ressiooinf  41981  fsumsermpt  42008  climexp  42034  climinf  42035  climsuse  42037  sumnnodd  42059  limsupresico  42129  limsupubuzlem  42141  limsupresxr  42195  liminfresxr  42196  liminfresico  42200  limsup10exlem  42201  cnrefiisplem  42258  cncfiooicclem1  42322  dvsinax  42342  itgsinexplem1  42383  fvvolioof  42418  fvvolicof  42420  stoweidlem14  42443  stoweidlem16  42445  stoweidlem31  42460  stoweidlem34  42463  stoweidlem36  42465  stoweidlem43  42472  stoweidlem46  42475  stoweidlem47  42476  stoweidlem52  42481  stoweidlem55  42484  stoweidlem57  42486  dirkercncf  42536  fourierdlem20  42556  fourierdlem42  42578  fourierdlem48  42583  fourierdlem49  42584  fourierdlem51  42586  fourierdlem54  42589  fourierdlem62  42597  fourierdlem71  42606  fourierdlem80  42615  fourierdlem114  42649  fouriersw  42660  ioorrnopnlem  42733  ioorrnopnxrlem  42735  salexct3  42769  salgencntex  42770  salgensscntex  42771  subsalsal  42786  sge0fodjrnlem  42842  sge0isum  42853  sge0seq  42872  sge0reuz  42873  sge0reuzb  42874  meadjiunlem  42891  meaiininclem  42912  carageniuncllem1  42947  caratheodorylem1  42952  hoiprodp1  43014  hoidmv1lelem1  43017  hoidmv1lelem2  43018  hoidmv1le  43020  hoidmvlelem1  43021  hoidmvlelem2  43022  hoidmvlelem3  43023  voncmpl  43047  hoiqssbl  43051  smflimlem2  43192  smfsuplem1  43229  smfsuplem3  43231  afvres  43515  afv2res  43582  fundcmpsurinjimaid  43715  iccpartigtl  43727  sprsymrelf  43799  prproropf1olem2  43808  ushrisomgr  44147  funcringcsetcALTV2lem3  44450  funcringcsetclem3ALTV  44473  lindslinindsimp2lem5  44658  rrxsphere  44918  line2  44922  onsetreclem3  44992  amgmwlem  45086
  Copyright terms: Public domain W3C validator