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  4859  elabrex  5759  fliftel1  5795  ovidig  5992  unielxp  6175  2oconcl  6440  ecopqsi  6590  eroprf  6628  exmidpweq  6909  sbthlem2  6957  djulclr  7048  djurclr  7049  djulcl  7050  djurcl  7051  caseinl  7090  caseinr  7091  ctssdccl  7110  isnumi  7181  addclnq  7374  mulclnq  7375  recexnq  7389  ltexnqq  7407  prarloclemarch  7417  prarloclemarch2  7418  nnnq  7421  nqnq0  7440  addclnq0  7450  mulclnq0  7451  nqpnq0nq  7452  prarloclemlt  7492  prarloclemlo  7493  prarloclemcalc  7501  nqprm  7541  cauappcvgprlem2  7659  caucvgprlem2  7679  addclsr  7752  mulclsr  7753  prsrcl  7783  mappsrprg  7803  suplocsrlemb  7805  pitonnlem2  7846  pitore  7849  recnnre  7850  axaddcl  7863  axmulcl  7865  axcaucvglemcl  7894  axcaucvglemval  7896  axcaucvglemcau  7897  axcaucvglemres  7898  uztrn2  9545  eluz2nn  9566  peano2uzs  9584  rebtwn2z  10255  seqf  10461  ser0  10514  bcm1k  10740  bcp1nk  10742  bcpasc  10746  hashennn  10760  hashcl  10761  climconst  11298  climshft2  11314  clim2ser  11345  clim2ser2  11346  iserex  11347  serf0  11360  zsumdc  11392  fsump1i  11441  iserabs  11483  isumshft  11498  isumsplit  11499  isum1p  11500  isumrpcl  11502  cvgratnnlemseq  11534  cvgratz  11540  cvgratgt0  11541  clim2prod  11547  clim2divap  11548  prodf1  11550  ntrivcvgap0  11557  zproddc  11587  fprodntrivap  11592  fprodabs  11624  fprodeq0  11625  ef0lem  11668  dvdsflip  11857  fzo0dvdseq  11863  gcdsupcl  11959  ialgr0  12044  prmind2  12120  crth  12224  prmdiv  12235  pockthlem  12354  pockthg  12355  prmunb  12360  ennnfonelemkh  12413  ennnfonelemrn  12420  ennnfonelemdm  12421  ctiunctlemf  12439  strslfv2d  12505  1strbas  12576  2strbasg  12578  2stropg  12579  2strbas1g  12581  rngbaseg  12594  rngplusgg  12595  rngmulrg  12596  srngbased  12605  srngplusgd  12606  srngmulrd  12607  srnginvld  12608  lmodbased  12623  lmodplusgd  12624  lmodscad  12625  lmodvscad  12626  ipsbased  12635  ipsaddgd  12636  ipsmulrd  12637  ipsscad  12638  ipsvscad  12639  ipsipd  12640  topgrpbasd  12652  topgrpplusgd  12653  topgrptsetd  12654  mulgnnp1  12991  lmconst  13719  lmss  13749  uptx  13777  cnmpt1res  13799  dvidlemap  14163  dvrecap  14180  pilem3  14207  logbleb  14382  logblt  14383  lgseisenlem1  14453  djulclALT  14556  djurclALT  14557  pwle2  14751  trilpolemeq1  14791