Theorem eleqtrrdi 2271

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 2181	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eleqtrdi 2270	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1353   ∈ wcel 2148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173

This theorem is referenced by:  brelrng  4860  elabrex  5760  elabrexg  5761  fliftel1  5797  ovidig  5994  unielxp  6177  2oconcl  6442  ecopqsi  6592  eroprf  6630  exmidpweq  6911  sbthlem2  6959  djulclr  7050  djurclr  7051  djulcl  7052  djurcl  7053  caseinl  7092  caseinr  7093  ctssdccl  7112  isnumi  7183  addclnq  7376  mulclnq  7377  recexnq  7391  ltexnqq  7409  prarloclemarch  7419  prarloclemarch2  7420  nnnq  7423  nqnq0  7442  addclnq0  7452  mulclnq0  7453  nqpnq0nq  7454  prarloclemlt  7494  prarloclemlo  7495  prarloclemcalc  7503  nqprm  7543  cauappcvgprlem2  7661  caucvgprlem2  7681  addclsr  7754  mulclsr  7755  prsrcl  7785  mappsrprg  7805  suplocsrlemb  7807  pitonnlem2  7848  pitore  7851  recnnre  7852  axaddcl  7865  axmulcl  7867  axcaucvglemcl  7896  axcaucvglemval  7898  axcaucvglemcau  7899  axcaucvglemres  7900  uztrn2  9547  eluz2nn  9568  peano2uzs  9586  rebtwn2z  10257  seqf  10463  ser0  10516  bcm1k  10742  bcp1nk  10744  bcpasc  10748  hashennn  10762  hashcl  10763  climconst  11300  climshft2  11316  clim2ser  11347  clim2ser2  11348  iserex  11349  serf0  11362  zsumdc  11394  fsump1i  11443  iserabs  11485  isumshft  11500  isumsplit  11501  isum1p  11502  isumrpcl  11504  cvgratnnlemseq  11536  cvgratz  11542  cvgratgt0  11543  clim2prod  11549  clim2divap  11550  prodf1  11552  ntrivcvgap0  11559  zproddc  11589  fprodntrivap  11594  fprodabs  11626  fprodeq0  11627  ef0lem  11670  dvdsflip  11859  fzo0dvdseq  11865  gcdsupcl  11961  ialgr0  12046  prmind2  12122  crth  12226  prmdiv  12237  pockthlem  12356  pockthg  12357  prmunb  12362  ennnfonelemkh  12415  ennnfonelemrn  12422  ennnfonelemdm  12423  ctiunctlemf  12441  strslfv2d  12507  1strbas  12578  2strbasg  12580  2stropg  12581  2strbas1g  12583  rngbaseg  12596  rngplusgg  12597  rngmulrg  12598  srngbased  12607  srngplusgd  12608  srngmulrd  12609  srnginvld  12610  lmodbased  12625  lmodplusgd  12626  lmodscad  12627  lmodvscad  12628  ipsbased  12637  ipsaddgd  12638  ipsmulrd  12639  ipsscad  12640  ipsvscad  12641  ipsipd  12642  topgrpbasd  12657  topgrpplusgd  12658  topgrptsetd  12659  mulgnnp1  12996  lmconst  13755  lmss  13785  uptx  13813  cnmpt1res  13835  dvidlemap  14199  dvrecap  14216  pilem3  14243  logbleb  14418  logblt  14419  lgseisenlem1  14489  djulclALT  14592  djurclALT  14593  pwle2  14787  trilpolemeq1  14827