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  3698  freccllem  6403  nninfisol  7131  finomni  7138  exmidomniim  7139  ismkvnex  7153  exmidaclem  7207  caucvgprprlem2  7709  gt0srpr  7747  eluzel2  9533  fseq1p1m1  10094  fznn0sub2  10128  nn0split  10136  nnsplit  10137  exple1  10576  bcval5  10743  bcpasc  10746  zfz1isolemsplit  10818  seq3coll  10822  clim2ser  11345  clim2ser2  11346  iserex  11347  isermulc2  11348  iserle  11350  iserge0  11351  climub  11352  climserle  11353  serf0  11360  summodclem3  11388  summodclem2a  11389  fsum3  11395  sum0  11396  fsumcl2lem  11406  fsumadd  11414  isumclim3  11431  isumadd  11439  fsump1i  11441  fsummulc2  11456  cvgcmpub  11484  binom1dif  11495  isumshft  11498  isumsplit  11499  isumrpcl  11502  arisum2  11507  trireciplem  11508  geoserap  11515  geolim  11519  geo2lim  11524  cvgratnnlemnexp  11532  cvgratnnlemseq  11534  cvgratgt0  11541  mertenslemi1  11543  mertenslem2  11544  mertensabs  11545  clim2prod  11547  clim2divap  11548  prodmodclem3  11583  prodmodclem2a  11584  fprodseq  11591  fprodntrivap  11592  fprodssdc  11598  fprodmul  11599  fprodabs  11624  fprodeq0  11625  efcvgfsum  11675  efcj  11681  effsumlt  11700  mod2eq1n2dvds  11884  algrp1  12046  phiprmpw  12222  crth  12224  phimullem  12225  prmdiv  12235  pcpremul  12293  pcmpt  12341  pcfac  12348  pockthlem  12354  pockthg  12355  1arith  12365  ennnfonelemp1  12407  nninfdclemp1  12451  mulgnnp1  12991  mulgnn0z  13010  mulgnndir  13012  istps  13535  topontopn  13540  cldrcl  13605  cnrehmeocntop  14096  lgsval2lem  14414  lgsdir2lem3  14434  lgsdir2lem5  14436  lgsdir  14439  lgsdilem2  14440  lgsdi  14441  lgsne0  14442  lgseisenlem1  14453  nnsf  14757  nninfsellemqall  14767  nninfomnilem  14770  cvgcmp2nlemabs  14783  trilpolemeq1  14791  nconstwlpolemgt0  14814