Theorem eleqtrd 2275

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 2266	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ 𝐶))
4	1, 3	mpbid 147	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

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

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178

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

This theorem is referenced by:  eleqtrrd  2276  3eltr3d  2279  eleqtrid  2285  eleqtrdi  2289  opth1  4270  0nelop  4282  tfisi  4624  nnpredlt  4661  iotam  5251  ercl  6604  erth  6639  ecelqsdm  6665  phpm  6927  exmidpweq  6971  cc2lem  7335  cc3  7337  suplocexprlemmu  7787  suplocexprlemloc  7790  lincmb01cmp  10080  fzopth  10138  fzoaddel2  10271  fzosubel2  10273  fzocatel  10277  zpnn0elfzo1  10286  fzoend  10300  peano2fzor  10310  monoord2  10580  ser3mono  10581  bcpasc  10860  zfz1isolemiso  10933  fisum0diag2  11614  isumsplit  11658  prodmodclem3  11742  prodmodclem2a  11743  nnmindc  12211  nnminle  12212  basmexd  12748  basm  12749  mgm1  13023  grpidd  13036  gsumress  13048  sgrppropd  13066  ismndd  13088  mndpropd  13091  issubmnd  13093  grpidd2  13183  imasgrp  13251  submmulg  13306  subginvcl  13323  subgcl  13324  subgsub  13326  subgmulg  13328  1nsgtrivd  13359  quseccl0g  13371  kerf1ghm  13414  rngass  13505  rngcl  13510  rngpropd  13521  imasrng  13522  srgcl  13536  srgass  13537  srg1zr  13553  srgpcomp  13556  srgpcompp  13557  srgpcomppsc  13558  crngcom  13580  ringass  13582  ringidmlem  13588  ringidss  13595  ringpropd  13604  imasring  13630  qusring2  13632  mulgass3  13651  dvdsrd  13660  1unit  13673  unitmulcl  13679  dvrvald  13700  rdivmuldivd  13710  elrhmunit  13743  rhmunitinv  13744  lringuplu  13762  subrngmcl  13775  subrg1  13797  subrgmcl  13799  subrgdv  13804  subrgunit  13805  resrhm  13814  aprval  13848  aprirr  13849  aprsym  13850  aprcotr  13851  lmodprop2d  13914  lidlss  14042  lidl0cl  14049  lidlacl  14050  lidlnegcl  14051  rnglidlmsgrp  14063  2idllidld  14072  2idlridld  14073  2idlcpblrng  14089  qus1  14092  quscrng  14099  rspsn  14100  znf1o  14217  psrelbas  14238  iscnp4  14464  cnrest2r  14483  txbasval  14513  txlm  14525  xmetunirn  14604  xblss2ps  14650  blbas  14679  mopntopon  14689  isxms2  14698  metcnpi  14761  metcnpi2  14762  tgioo  14800  cncfmpt2fcntop  14845  limccl  14905  limcimolemlt  14910  limccnp2cntop  14923  dvmulxxbr  14948  dvcoapbr  14953  dvcjbr  14954  dvrecap  14959  plyaddlem1  14993  plymullem1  14994  plycoeid3  15003  lgseisenlem4  15324