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  3699  freccllem  6406  nninfisol  7134  finomni  7141  exmidomniim  7142  ismkvnex  7156  exmidaclem  7210  caucvgprprlem2  7712  gt0srpr  7750  eluzel2  9536  fseq1p1m1  10097  fznn0sub2  10131  nn0split  10139  nnsplit  10140  exple1  10579  bcval5  10746  bcpasc  10749  zfz1isolemsplit  10821  seq3coll  10825  clim2ser  11348  clim2ser2  11349  iserex  11350  isermulc2  11351  iserle  11353  iserge0  11354  climub  11355  climserle  11356  serf0  11363  summodclem3  11391  summodclem2a  11392  fsum3  11398  sum0  11399  fsumcl2lem  11409  fsumadd  11417  isumclim3  11434  isumadd  11442  fsump1i  11444  fsummulc2  11459  cvgcmpub  11487  binom1dif  11498  isumshft  11501  isumsplit  11502  isumrpcl  11505  arisum2  11510  trireciplem  11511  geoserap  11518  geolim  11522  geo2lim  11527  cvgratnnlemnexp  11535  cvgratnnlemseq  11537  cvgratgt0  11544  mertenslemi1  11546  mertenslem2  11547  mertensabs  11548  clim2prod  11550  clim2divap  11551  prodmodclem3  11586  prodmodclem2a  11587  fprodseq  11594  fprodntrivap  11595  fprodssdc  11601  fprodmul  11602  fprodabs  11627  fprodeq0  11628  efcvgfsum  11678  efcj  11684  effsumlt  11703  mod2eq1n2dvds  11887  algrp1  12049  phiprmpw  12225  crth  12227  phimullem  12228  prmdiv  12238  pcpremul  12296  pcmpt  12344  pcfac  12351  pockthlem  12357  pockthg  12358  1arith  12368  ennnfonelemp1  12410  nninfdclemp1  12454  mulgnnp1  12997  mulgnn0z  13016  mulgnndir  13018  lspprid2  13504  istps  13672  topontopn  13677  cldrcl  13742  cnrehmeocntop  14233  lgsval2lem  14551  lgsdir2lem3  14571  lgsdir2lem5  14573  lgsdir  14576  lgsdilem2  14577  lgsdi  14578  lgsne0  14579  lgseisenlem1  14590  nnsf  14894  nninfsellemqall  14904  nninfomnilem  14907  cvgcmp2nlemabs  14920  trilpolemeq1  14928  nconstwlpolemgt0  14952