Theorem eleqtrd 2256

Description: Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)

Hypotheses

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

Assertion

Ref	Expression
eleqtrd	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Proof of Theorem eleqtrd

Step	Hyp	Ref	Expression
1		eleqtrd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
2		eleqtrd.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐶)
3	2	eleq2d 2247	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ 𝐶))
4	1, 3	mpbid 147	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:  eleqtrrd  2257  3eltr3d  2260  eleqtrid  2266  eleqtrdi  2270  opth1  4238  0nelop  4250  tfisi  4588  nnpredlt  4625  iotam  5210  ercl  6548  erth  6581  ecelqsdm  6607  phpm  6867  exmidpweq  6911  cc2lem  7267  cc3  7269  suplocexprlemmu  7719  suplocexprlemloc  7722  lincmb01cmp  10005  fzopth  10063  fzoaddel2  10195  fzosubel2  10197  fzocatel  10201  zpnn0elfzo1  10210  fzoend  10224  peano2fzor  10234  monoord2  10479  ser3mono  10480  bcpasc  10748  zfz1isolemiso  10821  fisum0diag2  11457  isumsplit  11501  prodmodclem3  11585  prodmodclem2a  11586  nnmindc  12037  nnminle  12038  basmexd  12524  mgm1  12794  grpidd  12807  ismndd  12843  mndpropd  12846  issubmnd  12848  grpidd2  12919  subginvcl  13048  subgcl  13049  subgsub  13051  subgmulg  13053  1nsgtrivd  13084  srgcl  13158  srgass  13159  srg1zr  13175  srgpcomp  13178  srgpcompp  13179  srgpcomppsc  13180  crngcom  13202  ringass  13204  ringidmlem  13210  ringidss  13217  ringpropd  13222  mulgass3  13259  dvdsrd  13268  1unit  13281  unitmulcl  13287  dvrvald  13308  rdivmuldivd  13318  lringuplu  13342  subrg1  13357  subrgmcl  13359  subrgdv  13364  subrgunit  13365  aprval  13377  aprirr  13378  aprsym  13379  aprcotr  13380  lmodprop2d  13443  iscnp4  13803  cnrest2r  13822  txbasval  13852  txlm  13864  xmetunirn  13943  xblss2ps  13989  blbas  14018  mopntopon  14028  isxms2  14037  metcnpi  14100  metcnpi2  14101  tgioo  14131  cncfmpt2fcntop  14170  limccl  14213  limcimolemlt  14218  limccnp2cntop  14231  dvmulxxbr  14251  dvcoapbr  14256  dvcjbr  14257  dvrecap  14262