Theorem eleqtrrdi 2325

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

Syntax hints:   → wi 4   = wceq 1398   ∈ wcel 2202

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227

This theorem is referenced by:  brelrng  4969  elabrex  5908  elabrexg  5909  fliftel1  5945  ovidig  6149  unielxp  6346  2oconcl  6650  ecopqsi  6802  eroprf  6840  exmidpweq  7144  sbthlem2  7200  djulclr  7291  djurclr  7292  djulcl  7293  djurcl  7294  caseinl  7333  caseinr  7334  ctssdccl  7353  isnumi  7429  addclnq  7638  mulclnq  7639  recexnq  7653  ltexnqq  7671  prarloclemarch  7681  prarloclemarch2  7682  nnnq  7685  nqnq0  7704  addclnq0  7714  mulclnq0  7715  nqpnq0nq  7716  prarloclemlt  7756  prarloclemlo  7757  prarloclemcalc  7765  nqprm  7805  cauappcvgprlem2  7923  caucvgprlem2  7943  addclsr  8016  mulclsr  8017  prsrcl  8047  mappsrprg  8067  suplocsrlemb  8069  pitonnlem2  8110  pitore  8113  recnnre  8114  axaddcl  8127  axmulcl  8129  axcaucvglemcl  8158  axcaucvglemval  8160  axcaucvglemcau  8161  axcaucvglemres  8162  uztrn2  9818  eluz2nn  9844  peano2uzs  9862  rebtwn2z  10560  seqf  10772  ser0  10841  bcm1k  11068  bcp1nk  11070  bcpasc  11074  hashennn  11088  hashcl  11089  climconst  11913  climshft2  11929  clim2ser  11960  clim2ser2  11961  iserex  11962  serf0  11975  zsumdc  12008  fsump1i  12057  iserabs  12099  isumshft  12114  isumsplit  12115  isum1p  12116  isumrpcl  12118  cvgratnnlemseq  12150  cvgratz  12156  cvgratgt0  12157  clim2prod  12163  clim2divap  12164  prodf1  12166  ntrivcvgap0  12173  zproddc  12203  fprodntrivap  12208  fprodabs  12240  fprodeq0  12241  ef0lem  12284  dvdsflip  12475  fzo0dvdseq  12481  bitsinv1  12586  gcdsupcl  12592  nninfctlemfo  12674  ialgr0  12679  prmind2  12755  crth  12859  prmdiv  12870  pockthlem  12992  pockthg  12993  prmunb  12998  ennnfonelemkh  13096  ennnfonelemrn  13103  ennnfonelemdm  13104  ctiunctlemf  13122  strslfv2d  13188  bassetsnn  13202  1strbas  13263  2strbasg  13266  2stropg  13267  2strbas1g  13269  rngbaseg  13282  rngplusgg  13283  rngmulrg  13284  srngbased  13293  srngplusgd  13294  srngmulrd  13295  srnginvld  13296  lmodbased  13311  lmodplusgd  13312  lmodscad  13313  lmodvscad  13314  ipsbased  13323  ipsaddgd  13324  ipsmulrd  13325  ipsscad  13326  ipsvscad  13327  ipsipd  13328  topgrpbasd  13343  topgrpplusgd  13344  topgrptsetd  13345  mulgnnp1  13780  znf1o  14730  lmconst  15010  lmss  15040  uptx  15068  cnmpt1res  15090  dvidlemap  15485  dvidrelem  15486  dvrecap  15507  plycolemc  15552  plycn  15556  pilem3  15577  logbleb  15755  logblt  15756  lgseisenlem1  15872  structvtxval  15963  ushgredgedgloop  16152  subgruhgredgdm  16194  wlkvtxm  16264  wlk1walkdom  16283  depindlem2  16431  djulclALT  16502  djurclALT  16503  pwle2  16703  trilpolemeq1  16755