Theorem eleqtrdi 2298

Description: A membership and equality inference. (Contributed by NM, 4-Jan-2006.)

Hypotheses

Ref	Expression
eleqtrdi.1	⊢ (𝜑 → 𝐴 ∈ 𝐵)
eleqtrdi.2	⊢ 𝐵 = 𝐶

Assertion

Ref	Expression
eleqtrdi	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Proof of Theorem eleqtrdi

Step	Hyp	Ref	Expression
1		eleqtrdi.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
2		eleqtrdi.2	. . 3 ⊢ 𝐵 = 𝐶
3	2	a1i 9	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	eleqtrd 2284	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

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

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-clel 2201

This theorem is referenced by:  eleqtrrdi  2299  prid2g  3738  freccllem  6488  nninfisol  7235  finomni  7242  exmidomniim  7243  ismkvnex  7257  exmidaclem  7320  caucvgprprlem2  7823  gt0srpr  7861  eluzel2  9653  fseq1p1m1  10216  fznn0sub2  10250  nn0split  10258  nnsplit  10259  exple1  10740  bcval5  10908  bcpasc  10911  zfz1isolemsplit  10983  seq3coll  10987  ccatrn  11065  swrdccat2  11124  clim2ser  11648  clim2ser2  11649  iserex  11650  isermulc2  11651  iserle  11653  iserge0  11654  climub  11655  climserle  11656  serf0  11663  summodclem3  11691  summodclem2a  11692  fsum3  11698  sum0  11699  fsumcl2lem  11709  fsumadd  11717  isumclim3  11734  isumadd  11742  fsump1i  11744  fsummulc2  11759  cvgcmpub  11787  binom1dif  11798  isumshft  11801  isumsplit  11802  isumrpcl  11805  arisum2  11810  trireciplem  11811  geoserap  11818  geolim  11822  geo2lim  11827  cvgratnnlemnexp  11835  cvgratnnlemseq  11837  cvgratgt0  11844  mertenslemi1  11846  mertenslem2  11847  mertensabs  11848  clim2prod  11850  clim2divap  11851  prodmodclem3  11886  prodmodclem2a  11887  fprodseq  11894  fprodntrivap  11895  fprodssdc  11901  fprodmul  11902  fprodabs  11927  fprodeq0  11928  efcvgfsum  11978  efcj  11984  effsumlt  12003  mod2eq1n2dvds  12190  bitsfzolem  12265  bitsfzo  12266  bitsfi  12268  bitsinv1lem  12272  bitsinv1  12273  nninfctlemfo  12361  algrp1  12368  phiprmpw  12544  crth  12546  phimullem  12547  prmdiv  12557  pcpremul  12616  pcmpt  12666  pcfac  12673  pockthlem  12679  pockthg  12680  1arith  12690  ennnfonelemp1  12777  nninfdclemp1  12821  relelbasov  12894  gsumwsubmcl  13328  gsumwmhm  13330  mulgnnp1  13466  mulgnn0z  13485  mulgnndir  13487  idomdomd  14039  idomcringd  14040  lspprid2  14174  istps  14504  topontopn  14509  cldrcl  14574  cnrehmeocntop  15082  elplyd  15213  ply1termlem  15214  ply1term  15215  plyaddlem1  15219  plymullem1  15220  plyaddlem  15221  plymullem  15222  plycoeid3  15229  plycolemc  15230  plycj  15233  dvply1  15237  0sgmppw  15465  1sgmprm  15466  lgsval2lem  15487  lgsdir2lem3  15507  lgsdir2lem5  15509  lgsdir  15512  lgsdilem2  15513  lgsdi  15514  lgsne0  15515  gausslemma2dlem3  15540  lgseisenlem1  15547  lgseisenlem4  15550  lgsquadlem2  15555  2omap  15932  nnsf  15942  nninfsellemqall  15952  nninfomnilem  15955  nnnninfex  15959  nninfnfiinf  15960  cvgcmp2nlemabs  15971  trilpolemeq1  15979  nconstwlpolemgt0  16003