Theorem eleqtrrdi 2290

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

Syntax hints:   → wi 4   = wceq 1364   ∈ wcel 2167

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-clel 2192

This theorem is referenced by:  brelrng  4898  elabrex  5807  elabrexg  5808  fliftel1  5844  ovidig  6044  unielxp  6241  2oconcl  6506  ecopqsi  6658  eroprf  6696  exmidpweq  6979  sbthlem2  7033  djulclr  7124  djurclr  7125  djulcl  7126  djurcl  7127  caseinl  7166  caseinr  7167  ctssdccl  7186  isnumi  7262  addclnq  7461  mulclnq  7462  recexnq  7476  ltexnqq  7494  prarloclemarch  7504  prarloclemarch2  7505  nnnq  7508  nqnq0  7527  addclnq0  7537  mulclnq0  7538  nqpnq0nq  7539  prarloclemlt  7579  prarloclemlo  7580  prarloclemcalc  7588  nqprm  7628  cauappcvgprlem2  7746  caucvgprlem2  7766  addclsr  7839  mulclsr  7840  prsrcl  7870  mappsrprg  7890  suplocsrlemb  7892  pitonnlem2  7933  pitore  7936  recnnre  7937  axaddcl  7950  axmulcl  7952  axcaucvglemcl  7981  axcaucvglemval  7983  axcaucvglemcau  7984  axcaucvglemres  7985  uztrn2  9638  eluz2nn  9659  peano2uzs  9677  rebtwn2z  10363  seqf  10575  ser0  10644  bcm1k  10871  bcp1nk  10873  bcpasc  10877  hashennn  10891  hashcl  10892  climconst  11474  climshft2  11490  clim2ser  11521  clim2ser2  11522  iserex  11523  serf0  11536  zsumdc  11568  fsump1i  11617  iserabs  11659  isumshft  11674  isumsplit  11675  isum1p  11676  isumrpcl  11678  cvgratnnlemseq  11710  cvgratz  11716  cvgratgt0  11717  clim2prod  11723  clim2divap  11724  prodf1  11726  ntrivcvgap0  11733  zproddc  11763  fprodntrivap  11768  fprodabs  11800  fprodeq0  11801  ef0lem  11844  dvdsflip  12035  fzo0dvdseq  12041  bitsinv1  12146  gcdsupcl  12152  nninfctlemfo  12234  ialgr0  12239  prmind2  12315  crth  12419  prmdiv  12430  pockthlem  12552  pockthg  12553  prmunb  12558  ennnfonelemkh  12656  ennnfonelemrn  12663  ennnfonelemdm  12664  ctiunctlemf  12682  strslfv2d  12748  1strbas  12822  2strbasg  12824  2stropg  12825  2strbas1g  12827  rngbaseg  12840  rngplusgg  12841  rngmulrg  12842  srngbased  12851  srngplusgd  12852  srngmulrd  12853  srnginvld  12854  lmodbased  12869  lmodplusgd  12870  lmodscad  12871  lmodvscad  12872  ipsbased  12881  ipsaddgd  12882  ipsmulrd  12883  ipsscad  12884  ipsvscad  12885  ipsipd  12886  topgrpbasd  12901  topgrpplusgd  12902  topgrptsetd  12903  mulgnnp1  13338  znf1o  14285  lmconst  14560  lmss  14590  uptx  14618  cnmpt1res  14640  dvidlemap  15035  dvidrelem  15036  dvrecap  15057  plycolemc  15102  plycn  15106  pilem3  15127  logbleb  15305  logblt  15306  lgseisenlem1  15419  djulclALT  15555  djurclALT  15556  pwle2  15753  trilpolemeq1  15797