Theorem eleqtrrdi 2332

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402   ∈ wcel 2209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  brelrng  5015  elabrex  5966  elabrexg  5967  fliftel1  6003  ovidig  6209  unielxp  6412  2oconcl  6716  ecopqsi  6868  eroprf  6906  exmidpweq  7220  sbthlem2  7280  djulclr  7395  djurclr  7396  djulcl  7397  djurcl  7398  caseinl  7437  caseinr  7438  ctssdccl  7457  isnumi  7533  addclnq  7748  mulclnq  7749  recexnq  7763  ltexnqq  7781  prarloclemarch  7791  prarloclemarch2  7792  nnnq  7795  nqnq0  7814  addclnq0  7824  mulclnq0  7825  nqpnq0nq  7826  prarloclemlt  7866  prarloclemlo  7867  prarloclemcalc  7875  nqprm  7915  cauappcvgprlem2  8033  caucvgprlem2  8053  addclsr  8126  mulclsr  8127  prsrcl  8157  mappsrprg  8177  suplocsrlemb  8179  pitonnlem2  8220  pitore  8223  recnnre  8224  axaddcl  8237  axmulcl  8239  axcaucvglemcl  8268  axcaucvglemval  8270  axcaucvglemcau  8271  axcaucvglemres  8272  uztrn2  9956  eluz2nn  9982  peano2uzs  10000  rebtwn2z  10706  seqf  10922  ser0  10991  bcm1k  11220  bcp1nk  11222  bcpasc  11226  hashennn  11241  hashcl  11242  climconst  12081  climshft2  12097  clim2ser  12128  clim2ser2  12129  iserex  12130  serf0  12143  zsumdc  12176  fsump1i  12225  iserabs  12267  isumshft  12282  isumsplit  12283  isum1p  12284  isumrpcl  12286  cvgratnnlemseq  12318  cvgratz  12324  cvgratgt0  12325  clim2prod  12331  clim2divap  12332  prodf1  12334  ntrivcvgap0  12341  zproddc  12371  fprodntrivap  12376  fprodabs  12408  fprodeq0  12409  ef0lem  12452  dvdsflip  12643  fzo0dvdseq  12649  bitsinv1  12754  gcdsupcl  12760  nninfctlemfo  12842  ialgr0  12847  prmind2  12923  crth  13031  prmdiv  13042  pockthlem  13164  pockthg  13165  prmunb  13170  ennnfonelemkh  13361  ennnfonelemrn  13368  ennnfonelemdm  13369  ctiunctlemf  13387  strslfv2d  13453  bassetsnn  13467  1strbas  13530  2strbasg  13533  2stropg  13534  2strbas1g  13536  rngbaseg  13549  rngplusgg  13550  rngmulrg  13551  srngbased  13560  srngplusgd  13561  srngmulrd  13562  srnginvld  13563  lmodbased  13578  lmodplusgd  13579  lmodscad  13580  lmodvscad  13581  ipsbased  13590  ipsaddgd  13591  ipsmulrd  13592  ipsscad  13593  ipsvscad  13594  ipsipd  13595  topgrpbasd  13610  topgrpplusgd  13611  topgrptsetd  13612  mulgnnp1  13992  cntrsubgnsg  14175  znf1o  15095  lmconst  15442  lmss  15472  uptx  15500  cnmpt1res  15522  dvidlemap  15917  dvidrelem  15918  dvrecap  15939  plycolemc  15984  plycn  15988  pilem3  16010  logbleb  16197  logblt  16198  ppiqub  16293  chtqub  16296  lgseisenlem1  16394  structvtxval  16485  ushgredgedgloop  16674  subgruhgredgdm  16716  wlkvtxm  16786  wlk1walkdom  16805  depindlem2  16953  djulclALT  17034  djurclALT  17035  pwle2  17233  idjudju  17252  trilpolemeq1  17296