Theorem eleqtrrdi 2233

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

Syntax hints:   → wi 4   = wceq 1331   ∈ wcel 1480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135

This theorem is referenced by:  brelrng  4770  elabrex  5659  fliftel1  5695  ovidig  5888  unielxp  6072  2oconcl  6336  ecopqsi  6484  eroprf  6522  sbthlem2  6846  djulclr  6934  djurclr  6935  djulcl  6936  djurcl  6937  caseinl  6976  caseinr  6977  ctssdccl  6996  isnumi  7038  addclnq  7183  mulclnq  7184  recexnq  7198  ltexnqq  7216  prarloclemarch  7226  prarloclemarch2  7227  nnnq  7230  nqnq0  7249  addclnq0  7259  mulclnq0  7260  nqpnq0nq  7261  prarloclemlt  7301  prarloclemlo  7302  prarloclemcalc  7310  nqprm  7350  cauappcvgprlem2  7468  caucvgprlem2  7488  addclsr  7561  mulclsr  7562  prsrcl  7592  mappsrprg  7612  suplocsrlemb  7614  pitonnlem2  7655  pitore  7658  recnnre  7659  axaddcl  7672  axmulcl  7674  axcaucvglemcl  7703  axcaucvglemval  7705  axcaucvglemcau  7706  axcaucvglemres  7707  uztrn2  9343  eluz2nn  9364  peano2uzs  9379  rebtwn2z  10032  seqf  10234  ser0  10287  bcm1k  10506  bcp1nk  10508  bcpasc  10512  hashennn  10526  hashcl  10527  climconst  11059  climshft2  11075  clim2ser  11106  clim2ser2  11107  iserex  11108  serf0  11121  zsumdc  11153  fsump1i  11202  iserabs  11244  isumshft  11259  isumsplit  11260  isum1p  11261  isumrpcl  11263  cvgratnnlemseq  11295  cvgratz  11301  cvgratgt0  11302  clim2prod  11308  clim2divap  11309  prodf1  11311  ntrivcvgap0  11318  ef0lem  11366  dvdsflip  11549  fzo0dvdseq  11555  gcdsupcl  11647  ialgr0  11725  prmind2  11801  crth  11900  ennnfonelemkh  11925  ennnfonelemrn  11932  ennnfonelemdm  11933  ctiunctlemf  11951  strslfv2d  12001  1strbas  12058  2strbasg  12060  2stropg  12061  2strbas1g  12063  rngbaseg  12075  rngplusgg  12076  rngmulrg  12077  srngbased  12082  srngplusgd  12083  srngmulrd  12084  srnginvld  12085  lmodbased  12093  lmodplusgd  12094  lmodscad  12095  lmodvscad  12096  ipsbased  12101  ipsaddgd  12102  ipsmulrd  12103  ipsscad  12104  ipsvscad  12105  ipsipd  12106  topgrpbasd  12111  topgrpplusgd  12112  topgrptsetd  12113  lmconst  12385  lmss  12415  uptx  12443  cnmpt1res  12465  dvidlemap  12829  dvrecap  12846  pilem3  12864  djulclALT  13008  djurclALT  13009  pwle2  13193  trilpolemeq1  13233