Theorem eleqtrrdi 2332

Description: A membership and equality inference. (Contributed by NM, 24-Apr-2005.)

Hypotheses

Ref	Expression
eleqtrrdi.1	|- ( ph -> A e. B )
eleqtrrdi.2	|- C = B

Assertion

Ref	Expression
eleqtrrdi	|- ( ph -> A e. C )

Proof of Theorem eleqtrrdi

Step	Hyp	Ref	Expression
1		eleqtrrdi.1	. 2 |- ( ph -> A e. B )
2		eleqtrrdi.2	. . 3 |- C = B
3	2	eqcomi 2242	. 2 |- B = C
4	1, 3	eleqtrdi 2331	1 |- ( ph -> A e. C )

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   e. 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  6717  ecopqsi  6869  eroprf  6907  exmidpweq  7222  sbthlem2  7282  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  9955  eluz2nn  9981  peano2uzs  9999  rebtwn2z  10705  seqf  10921  ser0  10990  bcm1k  11219  bcp1nk  11221  bcpasc  11225  hashennn  11240  hashcl  11241  climconst  12080  climshft2  12096  clim2ser  12127  clim2ser2  12128  iserex  12129  serf0  12142  zsumdc  12175  fsump1i  12224  iserabs  12266  isumshft  12281  isumsplit  12282  isum1p  12283  isumrpcl  12285  cvgratnnlemseq  12317  cvgratz  12323  cvgratgt0  12324  clim2prod  12330  clim2divap  12331  prodf1  12333  ntrivcvgap0  12340  zproddc  12370  fprodntrivap  12375  fprodabs  12407  fprodeq0  12408  ef0lem  12451  dvdsflip  12642  fzo0dvdseq  12648  bitsinv1  12753  gcdsupcl  12759  nninfctlemfo  12841  ialgr0  12846  prmind2  12922  crth  13030  prmdiv  13041  pockthlem  13163  pockthg  13164  prmunb  13169  ennnfonelemkh  13360  ennnfonelemrn  13367  ennnfonelemdm  13368  ctiunctlemf  13386  strslfv2d  13452  bassetsnn  13466  1strbas  13529  2strbasg  13532  2stropg  13533  2strbas1g  13535  rngbaseg  13548  rngplusgg  13549  rngmulrg  13550  srngbased  13559  srngplusgd  13560  srngmulrd  13561  srnginvld  13562  lmodbased  13577  lmodplusgd  13578  lmodscad  13579  lmodvscad  13580  ipsbased  13589  ipsaddgd  13590  ipsmulrd  13591  ipsscad  13592  ipsvscad  13593  ipsipd  13594  topgrpbasd  13609  topgrpplusgd  13610  topgrptsetd  13611  mulgnnp1  13991  cntrsubgnsg  14174  znf1o  15094  lmconst  15459  lmss  15489  uptx  15517  cnmpt1res  15539  dvidlemap  15934  dvidrelem  15935  dvrecap  15956  plycolemc  16001  plycn  16005  pilem3  16027  logbleb  16214  logblt  16215  ppiqub  16310  chtqub  16313  lgseisenlem1  16411  structvtxval  16502  ushgredgedgloop  16691  subgruhgredgdm  16733  wlkvtxm  16803  wlk1walkdom  16822  depindlem2  16970  djulclALT  17051  djurclALT  17052  pwle2  17250  idjudju  17269  trilpolemeq1  17313