Theorem eleqtrd 2317

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402   ∈ wcel 2209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  eleqtrrd  2318  3eltr3d  2321  eleqtrid  2327  eleqtrdi  2331  opth1  4376  0nelop  4388  tfisi  4734  nnpredlt  4771  iotam  5369  ercl  6818  erth  6853  ecelqsdm  6879  phpm  7167  exmidpweq  7216  pw1if  7584  cc2lem  7632  cc3  7634  suplocexprlemmu  8085  suplocexprlemloc  8088  lincmb01cmp  10405  fzopth  10467  fzoaddel2  10608  fzosubel2  10613  fzocatel  10617  zpnn0elfzo1  10626  fzoend  10640  peano2fzor  10650  infssfzcldc  10669  infssfzledc  10670  monoord2  10923  ser3mono  10924  bcpasc  11204  zfz1isolemiso  11291  swrdclg  11422  fisum0diag2  12214  isumsplit  12258  prodmodclem3  12342  prodmodclem2a  12343  nnmindc  12811  nnminle  12812  bassetsnn  13409  basmexd  13413  basm  13414  slotm  13415  mgm1  13690  grpidd  13703  gzsumress  13712  sgrppropd  13728  ismndd  13750  mndpropd  13753  issubmnd  13755  imasmnd  13760  grpidd2  13846  imasgrp  13914  submmulg  13969  subginvcl  13986  subgcl  13987  subgsub  13989  subgmulg  13991  1nsgtrivd  14022  quseccl0g  14034  kerf1ghm  14077  prdsbasfn  14181  prdsbasprj  14182  pwsplusgval  14208  pwsmulrval  14209  pwsinvg  14215  rngass  14238  rngcl  14243  rngpropd  14254  imasrng  14255  srgcl  14274  srgass  14275  srgpcomp  14294  srgpcompp  14295  srgpcomppsc  14296  crngcom  14318  ringass  14320  ringidmlem  14327  ringidss  14334  ringpropd  14343  imasring  14369  qusring2  14371  mulgass3  14391  dvdsrd  14401  1unit  14414  unitmulcl  14420  dvrvald  14441  rdivmuldivd  14451  elrhmunit  14484  rhmunitinv  14485  lringuplu  14503  subrngmcl  14517  subrg1  14539  subrgmcl  14541  subrgdv  14546  subrgunit  14547  resrhm  14556  aprval  14591  aprirr  14595  aprsym  14596  aprcotr  14597  opprdrng  14620  lmodprop2d  14685  lidlss  14813  lidl0cl  14820  lidlacl  14821  lidlnegcl  14822  rnglidlmsgrp  14834  2idllidld  14843  2idlridld  14844  2idlcpblrng  14860  qus1  14863  quscrng  14870  rspsn  14871  znf1o  14986  assapropd  15014  psrbagfi  15059  psrelbas  15066  iscnp4  15319  cnrest2r  15338  txbasval  15368  txlm  15380  xmetunirn  15459  xblss2ps  15505  blbas  15534  mopntopon  15544  isxms2  15553  metcnpi  15616  metcnpi2  15617  tgioo  15655  cncfmpt2fcntop  15700  limccl  15760  limcimolemlt  15765  limccnp2cntop  15778  dvmulxxbr  15803  dvcoapbr  15808  dvcjbr  15809  dvrecap  15814  plyaddlem1  15848  plymullem1  15849  plycoeid3  15858  lgseisenlem4  16192  usgr1vr  16489  clwwlkccatlem  16641