Theorem eleqtrrdi 2301

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

Syntax hints:   → wi 4   = wceq 1373   ∈ wcel 2178

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-cleq 2200  df-clel 2203

This theorem is referenced by:  brelrng  4928  elabrex  5849  elabrexg  5850  fliftel1  5886  ovidig  6086  unielxp  6283  2oconcl  6548  ecopqsi  6700  eroprf  6738  exmidpweq  7032  sbthlem2  7086  djulclr  7177  djurclr  7178  djulcl  7179  djurcl  7180  caseinl  7219  caseinr  7220  ctssdccl  7239  isnumi  7315  addclnq  7523  mulclnq  7524  recexnq  7538  ltexnqq  7556  prarloclemarch  7566  prarloclemarch2  7567  nnnq  7570  nqnq0  7589  addclnq0  7599  mulclnq0  7600  nqpnq0nq  7601  prarloclemlt  7641  prarloclemlo  7642  prarloclemcalc  7650  nqprm  7690  cauappcvgprlem2  7808  caucvgprlem2  7828  addclsr  7901  mulclsr  7902  prsrcl  7932  mappsrprg  7952  suplocsrlemb  7954  pitonnlem2  7995  pitore  7998  recnnre  7999  axaddcl  8012  axmulcl  8014  axcaucvglemcl  8043  axcaucvglemval  8045  axcaucvglemcau  8046  axcaucvglemres  8047  uztrn2  9701  eluz2nn  9722  peano2uzs  9740  rebtwn2z  10434  seqf  10646  ser0  10715  bcm1k  10942  bcp1nk  10944  bcpasc  10948  hashennn  10962  hashcl  10963  climconst  11716  climshft2  11732  clim2ser  11763  clim2ser2  11764  iserex  11765  serf0  11778  zsumdc  11810  fsump1i  11859  iserabs  11901  isumshft  11916  isumsplit  11917  isum1p  11918  isumrpcl  11920  cvgratnnlemseq  11952  cvgratz  11958  cvgratgt0  11959  clim2prod  11965  clim2divap  11966  prodf1  11968  ntrivcvgap0  11975  zproddc  12005  fprodntrivap  12010  fprodabs  12042  fprodeq0  12043  ef0lem  12086  dvdsflip  12277  fzo0dvdseq  12283  bitsinv1  12388  gcdsupcl  12394  nninfctlemfo  12476  ialgr0  12481  prmind2  12557  crth  12661  prmdiv  12672  pockthlem  12794  pockthg  12795  prmunb  12800  ennnfonelemkh  12898  ennnfonelemrn  12905  ennnfonelemdm  12906  ctiunctlemf  12924  strslfv2d  12990  1strbas  13064  2strbasg  13067  2stropg  13068  2strbas1g  13070  rngbaseg  13083  rngplusgg  13084  rngmulrg  13085  srngbased  13094  srngplusgd  13095  srngmulrd  13096  srnginvld  13097  lmodbased  13112  lmodplusgd  13113  lmodscad  13114  lmodvscad  13115  ipsbased  13124  ipsaddgd  13125  ipsmulrd  13126  ipsscad  13127  ipsvscad  13128  ipsipd  13129  topgrpbasd  13144  topgrpplusgd  13145  topgrptsetd  13146  mulgnnp1  13581  znf1o  14528  lmconst  14803  lmss  14833  uptx  14861  cnmpt1res  14883  dvidlemap  15278  dvidrelem  15279  dvrecap  15300  plycolemc  15345  plycn  15349  pilem3  15370  logbleb  15548  logblt  15549  lgseisenlem1  15662  structvtxval  15753  djulclALT  15937  djurclALT  15938  pwle2  16137  trilpolemeq1  16181