Theorem eleqtrd 2268

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

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

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 2171

This theorem depends on definitions:  df-bi 117  df-cleq 2182  df-clel 2185

This theorem is referenced by:  eleqtrrd  2269  3eltr3d  2272  eleqtrid  2278  eleqtrdi  2282  opth1  4254  0nelop  4266  tfisi  4604  nnpredlt  4641  iotam  5227  ercl  6570  erth  6605  ecelqsdm  6631  phpm  6893  exmidpweq  6937  cc2lem  7295  cc3  7297  suplocexprlemmu  7747  suplocexprlemloc  7750  lincmb01cmp  10033  fzopth  10091  fzoaddel2  10223  fzosubel2  10225  fzocatel  10229  zpnn0elfzo1  10238  fzoend  10252  peano2fzor  10262  monoord2  10508  ser3mono  10509  bcpasc  10778  zfz1isolemiso  10851  fisum0diag2  11487  isumsplit  11531  prodmodclem3  11615  prodmodclem2a  11616  nnmindc  12067  nnminle  12068  basmexd  12572  basm  12573  mgm1  12846  grpidd  12859  sgrppropd  12876  ismndd  12898  mndpropd  12901  issubmnd  12903  grpidd2  12985  imasgrp  13053  subginvcl  13122  subgcl  13123  subgsub  13125  subgmulg  13127  1nsgtrivd  13158  quseccl0g  13170  kerf1ghm  13213  rngass  13293  rngcl  13298  rngpropd  13309  imasrng  13310  srgcl  13324  srgass  13325  srg1zr  13341  srgpcomp  13344  srgpcompp  13345  srgpcomppsc  13346  crngcom  13368  ringass  13370  ringidmlem  13376  ringidss  13383  ringpropd  13392  imasring  13414  qusring2  13416  mulgass3  13435  dvdsrd  13444  1unit  13457  unitmulcl  13463  dvrvald  13484  rdivmuldivd  13494  elrhmunit  13527  rhmunitinv  13528  lringuplu  13543  subrngmcl  13556  subrg1  13578  subrgmcl  13580  subrgdv  13585  subrgunit  13586  aprval  13598  aprirr  13599  aprsym  13600  aprcotr  13601  lmodprop2d  13664  lidlss  13792  lidl0cl  13799  lidlacl  13800  lidlnegcl  13801  rnglidlmsgrp  13813  2idllidld  13821  2idlridld  13822  2idlcpblrng  13838  qus1  13841  quscrng  13847  psrelbas  13952  iscnp4  14175  cnrest2r  14194  txbasval  14224  txlm  14236  xmetunirn  14315  xblss2ps  14361  blbas  14390  mopntopon  14400  isxms2  14409  metcnpi  14472  metcnpi2  14473  tgioo  14503  cncfmpt2fcntop  14542  limccl  14585  limcimolemlt  14590  limccnp2cntop  14603  dvmulxxbr  14623  dvcoapbr  14628  dvcjbr  14629  dvrecap  14634