Theorem eleqtrdi 2270

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 2256	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1353   ∈ wcel 2148

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173

This theorem is referenced by:  eleqtrrdi  2271  prid2g  3697  freccllem  6402  nninfisol  7130  finomni  7137  exmidomniim  7138  ismkvnex  7152  exmidaclem  7206  caucvgprprlem2  7708  gt0srpr  7746  eluzel2  9532  fseq1p1m1  10093  fznn0sub2  10127  nn0split  10135  nnsplit  10136  exple1  10575  bcval5  10742  bcpasc  10745  zfz1isolemsplit  10817  seq3coll  10821  clim2ser  11344  clim2ser2  11345  iserex  11346  isermulc2  11347  iserle  11349  iserge0  11350  climub  11351  climserle  11352  serf0  11359  summodclem3  11387  summodclem2a  11388  fsum3  11394  sum0  11395  fsumcl2lem  11405  fsumadd  11413  isumclim3  11430  isumadd  11438  fsump1i  11440  fsummulc2  11455  cvgcmpub  11483  binom1dif  11494  isumshft  11497  isumsplit  11498  isumrpcl  11501  arisum2  11506  trireciplem  11507  geoserap  11514  geolim  11518  geo2lim  11523  cvgratnnlemnexp  11531  cvgratnnlemseq  11533  cvgratgt0  11540  mertenslemi1  11542  mertenslem2  11543  mertensabs  11544  clim2prod  11546  clim2divap  11547  prodmodclem3  11582  prodmodclem2a  11583  fprodseq  11590  fprodntrivap  11591  fprodssdc  11597  fprodmul  11598  fprodabs  11623  fprodeq0  11624  efcvgfsum  11674  efcj  11680  effsumlt  11699  mod2eq1n2dvds  11883  algrp1  12045  phiprmpw  12221  crth  12223  phimullem  12224  prmdiv  12234  pcpremul  12292  pcmpt  12340  pcfac  12347  pockthlem  12353  pockthg  12354  1arith  12364  ennnfonelemp1  12406  nninfdclemp1  12450  mulgnnp1  12990  mulgnn0z  13008  mulgnndir  13010  istps  13502  topontopn  13507  cldrcl  13572  cnrehmeocntop  14063  lgsval2lem  14381  lgsdir2lem3  14401  lgsdir2lem5  14403  lgsdir  14406  lgsdilem2  14407  lgsdi  14408  lgsne0  14409  lgseisenlem1  14420  nnsf  14724  nninfsellemqall  14734  nninfomnilem  14737  cvgcmp2nlemabs  14750  trilpolemeq1  14758  nconstwlpolemgt0  14781