Theorem eleqtrrdi 2323

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

Syntax hints:   → wi 4   = wceq 1395   ∈ wcel 2200

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  brelrng  4954  elabrex  5880  elabrexg  5881  fliftel1  5917  ovidig  6121  unielxp  6318  2oconcl  6583  ecopqsi  6735  eroprf  6773  exmidpweq  7067  sbthlem2  7121  djulclr  7212  djurclr  7213  djulcl  7214  djurcl  7215  caseinl  7254  caseinr  7255  ctssdccl  7274  isnumi  7350  addclnq  7558  mulclnq  7559  recexnq  7573  ltexnqq  7591  prarloclemarch  7601  prarloclemarch2  7602  nnnq  7605  nqnq0  7624  addclnq0  7634  mulclnq0  7635  nqpnq0nq  7636  prarloclemlt  7676  prarloclemlo  7677  prarloclemcalc  7685  nqprm  7725  cauappcvgprlem2  7843  caucvgprlem2  7863  addclsr  7936  mulclsr  7937  prsrcl  7967  mappsrprg  7987  suplocsrlemb  7989  pitonnlem2  8030  pitore  8033  recnnre  8034  axaddcl  8047  axmulcl  8049  axcaucvglemcl  8078  axcaucvglemval  8080  axcaucvglemcau  8081  axcaucvglemres  8082  uztrn2  9736  eluz2nn  9757  peano2uzs  9775  rebtwn2z  10469  seqf  10681  ser0  10750  bcm1k  10977  bcp1nk  10979  bcpasc  10983  hashennn  10997  hashcl  10998  climconst  11796  climshft2  11812  clim2ser  11843  clim2ser2  11844  iserex  11845  serf0  11858  zsumdc  11890  fsump1i  11939  iserabs  11981  isumshft  11996  isumsplit  11997  isum1p  11998  isumrpcl  12000  cvgratnnlemseq  12032  cvgratz  12038  cvgratgt0  12039  clim2prod  12045  clim2divap  12046  prodf1  12048  ntrivcvgap0  12055  zproddc  12085  fprodntrivap  12090  fprodabs  12122  fprodeq0  12123  ef0lem  12166  dvdsflip  12357  fzo0dvdseq  12363  bitsinv1  12468  gcdsupcl  12474  nninfctlemfo  12556  ialgr0  12561  prmind2  12637  crth  12741  prmdiv  12752  pockthlem  12874  pockthg  12875  prmunb  12880  ennnfonelemkh  12978  ennnfonelemrn  12985  ennnfonelemdm  12986  ctiunctlemf  13004  strslfv2d  13070  bassetsnn  13084  1strbas  13145  2strbasg  13148  2stropg  13149  2strbas1g  13151  rngbaseg  13164  rngplusgg  13165  rngmulrg  13166  srngbased  13175  srngplusgd  13176  srngmulrd  13177  srnginvld  13178  lmodbased  13193  lmodplusgd  13194  lmodscad  13195  lmodvscad  13196  ipsbased  13205  ipsaddgd  13206  ipsmulrd  13207  ipsscad  13208  ipsvscad  13209  ipsipd  13210  topgrpbasd  13225  topgrpplusgd  13226  topgrptsetd  13227  mulgnnp1  13662  znf1o  14609  lmconst  14884  lmss  14914  uptx  14942  cnmpt1res  14964  dvidlemap  15359  dvidrelem  15360  dvrecap  15381  plycolemc  15426  plycn  15430  pilem3  15451  logbleb  15629  logblt  15630  lgseisenlem1  15743  structvtxval  15834  ushgredgedgloop  16020  djulclALT  16123  djurclALT  16124  pwle2  16323  trilpolemeq1  16367