Theorem eleqtrdi 2286

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

Syntax hints:   → wi 4   = wceq 1364   ∈ wcel 2164

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-cleq 2186  df-clel 2189

This theorem is referenced by:  eleqtrrdi  2287  prid2g  3724  freccllem  6457  nninfisol  7194  finomni  7201  exmidomniim  7202  ismkvnex  7216  exmidaclem  7270  caucvgprprlem2  7772  gt0srpr  7810  eluzel2  9600  fseq1p1m1  10163  fznn0sub2  10197  nn0split  10205  nnsplit  10206  exple1  10669  bcval5  10837  bcpasc  10840  zfz1isolemsplit  10912  seq3coll  10916  clim2ser  11483  clim2ser2  11484  iserex  11485  isermulc2  11486  iserle  11488  iserge0  11489  climub  11490  climserle  11491  serf0  11498  summodclem3  11526  summodclem2a  11527  fsum3  11533  sum0  11534  fsumcl2lem  11544  fsumadd  11552  isumclim3  11569  isumadd  11577  fsump1i  11579  fsummulc2  11594  cvgcmpub  11622  binom1dif  11633  isumshft  11636  isumsplit  11637  isumrpcl  11640  arisum2  11645  trireciplem  11646  geoserap  11653  geolim  11657  geo2lim  11662  cvgratnnlemnexp  11670  cvgratnnlemseq  11672  cvgratgt0  11679  mertenslemi1  11681  mertenslem2  11682  mertensabs  11683  clim2prod  11685  clim2divap  11686  prodmodclem3  11721  prodmodclem2a  11722  fprodseq  11729  fprodntrivap  11730  fprodssdc  11736  fprodmul  11737  fprodabs  11762  fprodeq0  11763  efcvgfsum  11813  efcj  11819  effsumlt  11838  mod2eq1n2dvds  12023  nninfctlemfo  12180  algrp1  12187  phiprmpw  12363  crth  12365  phimullem  12366  prmdiv  12376  pcpremul  12434  pcmpt  12484  pcfac  12491  pockthlem  12497  pockthg  12498  1arith  12508  ennnfonelemp1  12566  nninfdclemp1  12610  relelbasov  12683  gsumwsubmcl  13071  gsumwmhm  13073  mulgnnp1  13203  mulgnn0z  13222  mulgnndir  13224  idomdomd  13776  idomcringd  13777  lspprid2  13911  istps  14211  topontopn  14216  cldrcl  14281  cnrehmeocntop  14789  elplyd  14920  ply1termlem  14921  ply1term  14922  plyaddlem1  14926  plymullem1  14927  plyaddlem  14928  plymullem  14929  plycolemc  14936  plycj  14939  dvply1  14943  lgsval2lem  15167  lgsdir2lem3  15187  lgsdir2lem5  15189  lgsdir  15192  lgsdilem2  15193  lgsdi  15194  lgsne0  15195  gausslemma2dlem3  15220  lgseisenlem1  15227  lgseisenlem4  15230  lgsquadlem2  15235  nnsf  15565  nninfsellemqall  15575  nninfomnilem  15578  cvgcmp2nlemabs  15592  trilpolemeq1  15600  nconstwlpolemgt0  15624