Theorem eleqtrrdi 2850

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

Step	Hyp	Ref	Expression
1		eleqtrrdi.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
2		eleqtrrdi.2	. . 3 ⊢ 𝐶 = 𝐵
3	2	eqcomi 2747	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eleqtrdi 2849	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-clel 2817

This theorem is referenced by:  3eltr4g  2856  brelrng  5839  elabrex  7098  fliftel1  7161  ovidig  7393  unielxp  7842  tfrlem11  8190  rdglim  8228  seqomlem4  8254  2oconcl  8295  ecopqsi  8521  erov  8561  eroprf  8562  sbthlem2  8824  dffi3  9120  ixpiunwdom  9279  cantnfcl  9355  r1lim  9461  rankwflemb  9482  pwwf  9496  unwf  9499  rankwflem  9504  uniwf  9508  rankpwi  9512  rankr1g  9521  r1pw  9534  r1rankid  9548  rankuni  9552  djulcl  9599  djurcl  9600  inlresf  9603  inrresf  9605  djuun  9615  cardlim  9661  infxpenlem  9700  alephfp  9795  cfsmolem  9957  alephsing  9963  hsmexlem4  10116  axdc3lem2  10138  numth3  10157  iunfo  10226  konigthlem  10255  iunctb  10261  canthwelem  10337  canthwe  10338  r1limwun  10423  inar1  10462  inatsk  10465  gruina  10505  grur1  10507  tskmval  10526  tskmcl  10528  pinq  10614  dmrecnq  10655  addclsr  10770  mulclsr  10771  axaddf  10832  axmulf  10833  peano2nn  11915  uztrn2  12530  eluz2nn  12553  peano2uzs  12571  uzsupss  12609  uzsup  13511  uzrdgfni  13606  uzrdgsuci  13608  fsuppmapnn0fiub  13639  seqf  13672  ser0  13703  bcm1k  13957  bcp1nk  13959  bcpasc  13963  hashprdifel  14041  fz1isolem  14103  pr2pwpr  14121  ccats1val2  14262  rexuzre  14992  limsupgre  15118  climconst  15180  rlimclim1  15182  climrlim2  15184  clim2ser  15294  clim2ser2  15295  iserex  15296  isermulc2  15297  iserle  15299  isercolllem3  15306  isercoll2  15308  climsup  15309  iseraltlem2  15322  iseraltlem3  15323  zsum  15358  isumclim3  15399  isumadd  15407  fsump1i  15409  iserabs  15455  cvgcmp  15456  cvgcmpub  15457  cvgcmpce  15458  abscvgcvg  15459  isumshft  15479  isumsplit  15480  isum1p  15481  isumrpcl  15483  isumsup2  15486  climcndslem1  15489  cvgrat  15523  clim2prod  15528  clim2div  15529  prodf1  15531  ntrivcvgn0  15538  ntrivcvgtail  15540  fprodntriv  15580  fprodabs  15612  fprodeq0  15613  iprodclim3  15638  iprodmul  15641  ef0lem  15716  fprodefsum  15732  rpnnen2lem3  15853  dvdsflip  15954  fzo0dvdseq  15960  bitsinv1  16077  smupval  16123  smueqlem  16125  seq1st  16204  algr0  16205  prmind2  16318  crth  16407  eulerthlem2  16411  prmdiv  16414  pockthlem  16534  pockthg  16535  unbenlem  16537  prmunb  16543  prmgaplem7  16686  strfv2d  16831  imasvscaval  17166  oppccatid  17347  oppccatf  17356  epii  17372  fthepi  17560  funcestrcsetclem3  17775  funcsetcestrclem3  17789  yon12  17899  yon2  17900  yonedalem4c  17911  yonedalem22  17912  yonedalem3b  17913  yonedainv  17915  acsmapd  18187  mgm2nsgrplem1  18472  mgm2nsgrplem2  18473  mgm2nsgrplem3  18474  sgrp2nmndlem1  18477  sgrp2rid2  18480  cntrsubgnsg  18862  symgpssefmnd  18918  pmtrrn  18980  gexcl3  19107  efgi  19240  efgi2  19246  efgs1b  19257  efgredlemg  19263  efgredlemd  19265  frgpnabllem1  19389  cycsubgcyg  19417  gsumzaddlem  19437  dprdwd  19529  dprd2da  19560  lsppratlem3  20326  lsppratlem4  20327  lbsextlem2  20336  lidl0  20403  lidl1  20404  domnchr  20648  znf1o  20671  mplsubrglem  21120  mpfconst  21221  mpfproj  21222  mpfind  21227  mhpmulcl  21249  pf1const  21422  pf1id  21423  mpfpf1  21427  pf1mpf  21428  madetsumid  21518  slesolex  21739  pmatcoe1fsupp  21758  mat2pmatbas0  21784  pmatcollpw  21838  pm2mpf1  21856  isclo  22146  indiscld  22150  restntr  22241  ordtbaslem  22247  ordtbas2  22250  lmconst  22320  lmss  22357  conncompid  22490  2ndcomap  22517  locfincmp  22585  comppfsc  22591  xkouni  22658  txcls  22663  ptclsg  22674  uptx  22684  txindis  22693  tx1stc  22709  cnmpt1res  22735  tgqtop  22771  uffix  22980  cnpflf2  23059  ptcmplem2  23112  ptcmplem4  23114  tgpconncomp  23172  tsmsfbas  23187  fmucnd  23352  prdsxmetlem  23429  imasdsf1olem  23434  prdsbl  23553  blcvx  23867  xrsmopn  23881  xrge0tsms  23903  metdcn2  23908  expcncf  23995  cnmpopc  23997  icchmeo  24010  iccpnfhmeo  24014  cnheibor  24024  evth  24028  evth2  24029  lebnumlem2  24031  lebnumii  24035  reparphti  24066  cfilfcls  24343  minveclem2  24495  minveclem3  24498  minveclem4  24501  ovoliunlem1  24571  ovolicc1  24585  iundisj  24617  volsup  24625  uniioombllem3  24654  vitalilem2  24678  vitalilem3  24679  mbfsup  24733  mbfinf  24734  mbflimsup  24735  itg2monolem1  24820  limcflflem  24949  limccnp  24960  limccnp2  24961  dvidlem  24984  dvn2bss  24999  cpnres  25006  dvcobr  25015  dvrec  25024  c1liplem1  25065  dvcnvrelem2  25087  dvfsumrlimf  25094  dvfsumlem1  25095  dvfsumlem2  25096  dvfsumlem3  25097  dvfsumlem4  25098  dvfsumrlim  25100  dvfsum2  25103  coeeulem  25290  coeid3  25306  plycn  25327  dvntaylp  25435  taylthlem1  25437  taylthlem2  25438  ulm2  25449  ulmshftlem  25453  ulmshft  25454  ulm0  25455  ulmcn  25463  ulmdvlem3  25466  ulmdv  25467  mtest  25468  mtestbdd  25469  dvradcnv  25485  psercn2  25487  psercn  25490  pserdv  25493  abelth  25505  efif1olem2  25604  efif1olem4  25606  efifo  25608  eff1olem  25609  logcn  25707  dvloglem  25708  cxpcn3  25806  resqrtcn  25807  sqrtcn  25808  logbleb  25838  logblt  25839  asinneg  25941  atanlogsub  25971  atanbnd  25981  ressatans  25989  leibpilem2  25996  xrlimcnp  26023  efrlim  26024  scvxcvx  26040  ppiub  26257  chtub  26265  logexprlim  26278  lgseisenlem1  26428  rplogsumlem1  26537  rplogsumlem2  26538  dchrisumlem2  26543  dchrisum0flb  26563  logdivbnd  26609  pntlem3  26662  tgcgr4  26796  ltgov  26862  f1otrg  27136  eengtrkg  27257  iedgedg  27323  ushgredgedgloop  27501  subgruhgredgd  27554  uvtxupgrres  27678  umgr2v2evd2  27797  edginwlk  27904  wlk1walk  27908  crctcshwlkn0lem6  28081  wlkiswwlks1  28133  minvecolem1  29137  minvecolem2  29138  minvecolem4  29143  htthlem  29180  5oalem2  29918  3oalem2  29926  iundisjf  30829  fmptco1f1o  30869  xppreima  30884  xppreima2  30889  dfcnv2  30915  gsumhashmul  31218  xrge0tsmsd  31219  odpmco  31257  pmtrcnelor  31262  pmtrto1cl  31268  psgnfzto1stlem  31269  fzto1stfv1  31270  fzto1st  31272  fzto1stinvn  31273  psgnfzto1st  31274  tocycf  31286  cycpmco2lem7  31301  cycpmco2  31302  cycpmrn  31312  cyc3evpm  31319  cyc3genpmlem  31320  cycpmgcl  31322  cyc3conja  31326  rhmopp  31420  nsgmgc  31499  nsgqusf1olem1  31500  nsgqusf1olem2  31501  rhmpreimaprmidl  31529  ssmxidllem  31543  fply1  31569  smatlem  31649  smatcl  31654  zartopn  31727  zarmxt1  31732  tpr2rico  31764  xrmulc1cn  31782  xrge0mulc1cn  31793  esumpfinvallem  31942  ldgenpisyslem1  32031  dynkin  32035  brfae  32116  sxbrsigalem3  32139  dya2icoseg2  32145  omsmeas  32190  sibfof  32207  sseqmw  32258  sseqf  32259  sseqp1  32262  fiblem  32265  fibp1  32268  probfinmeasbALTV  32296  repr0  32491  reprpmtf1o  32506  hgt750lemg  32534  bnj1379  32710  srcmpltd  32954  subfacp1lem5  33046  subfacp1lem6  33047  cvxpconn  33104  cvxsconn  33105  cvmliftlem6  33152  cvmliftlem8  33154  cvmliftlem10  33156  cvmlift2lem6  33170  cvmlift2lem11  33175  cvmlift2lem12  33176  2goelgoanfmla1  33286  prv1n  33293  msubff  33392  msubco  33393  elmsta  33410  msubff1  33418  mvhf  33420  msubvrs  33422  iprodefisumlem  33612  filnetlem3  34496  knoppcnlem10  34609  knoppcnlem11  34610  icoreunrn  35457  icoreelrn  35459  ralssiun  35505  poimirlem3  35707  poimirlem16  35720  poimirlem17  35721  poimirlem19  35723  poimirlem30  35734  dvasin  35788  cover2  35799  upixp  35814  sdclem1  35828  fdc  35830  caushft  35846  ismtyres  35893  rrncmslem  35917  isfld2  36090  osumcllem10N  37906  pexmidlem7N  37917  dihglblem2N  39235  lcfrvalsnN  39482  lcfrlem5  39487  lcfrlem6  39488  lcfrlem27  39510  lcfrlem37  39520  prjspvs  40370  0prjspnrel  40385  monotuz  40679  expdiophlem1  40759  kelac2  40806  grurankcld  41740  dvgrat  41819  nzss  41824  uzmptshftfval  41853  binomcxplemnotnn0  41863  refsumcn  42462  rfcnpre2  42463  rfcnpre3  42465  rfcnpre4  42466  elabrexg  42478  disjf1o  42618  unirnmap  42637  unirnmapsn  42643  ssmapsn  42645  mptssid  42674  allbutfi  42823  eluzd  42839  uzidd2  42846  ressiocsup  42982  ressioosup  42983  ressiooinf  42985  fsumsermpt  43010  climexp  43036  climinf  43037  climsuse  43039  sumnnodd  43061  limsupresico  43131  limsupubuzlem  43143  limsupresxr  43197  liminfresxr  43198  liminfresico  43202  limsup10exlem  43203  cnrefiisplem  43260  cncfiooicclem1  43324  dvsinax  43344  itgsinexplem1  43385  fvvolioof  43420  fvvolicof  43422  stoweidlem14  43445  stoweidlem16  43447  stoweidlem31  43462  stoweidlem34  43465  stoweidlem36  43467  stoweidlem43  43474  stoweidlem46  43477  stoweidlem47  43478  stoweidlem52  43483  stoweidlem55  43486  stoweidlem57  43488  dirkercncf  43538  fourierdlem20  43558  fourierdlem42  43580  fourierdlem48  43585  fourierdlem49  43586  fourierdlem51  43588  fourierdlem54  43591  fourierdlem62  43599  fourierdlem71  43608  fourierdlem80  43617  fourierdlem114  43651  fouriersw  43662  ioorrnopnlem  43735  ioorrnopnxrlem  43737  salexct3  43771  salgencntex  43772  salgensscntex  43773  subsalsal  43788  sge0fodjrnlem  43844  sge0isum  43855  sge0seq  43874  sge0reuz  43875  sge0reuzb  43876  meadjiunlem  43893  meaiininclem  43914  carageniuncllem1  43949  caratheodorylem1  43954  hoiprodp1  44016  hoidmv1lelem1  44019  hoidmv1lelem2  44020  hoidmv1le  44022  hoidmvlelem1  44023  hoidmvlelem2  44024  hoidmvlelem3  44025  voncmpl  44049  hoiqssbl  44053  smflimlem2  44194  smfsuplem1  44231  smfsuplem3  44233  cfsetsnfsetf  44439  fcores  44448  afvres  44551  afv2res  44618  fundcmpsurinjimaid  44751  iccpartigtl  44763  sprsymrelf  44835  prproropf1olem2  44844  ushrisomgr  45181  funcringcsetcALTV2lem3  45484  funcringcsetclem3ALTV  45507  lindslinindsimp2lem5  45691  rrxsphere  45982  line2  45986  iooii  46099  icccldii  46100  iscnrm3rlem3  46124  onsetreclem3  46298  amgmwlem  46392