Theorem eqeltrd 2306

Description: Substitution of equal classes into membership relation, deduction form. (Contributed by Raph Levien, 10-Dec-2002.)

Hypotheses

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

Assertion

Ref	Expression
eqeltrd	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Proof of Theorem eqeltrd

Step	Hyp	Ref	Expression
1		eqeltrd.2	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝐶)
2		eqeltrd.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
3	2	eleq1d 2298	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))
4	1, 3	mpbird 167	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1395   ∈ wcel 2200

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  eqeltrrd  2307  3eltr4d  2313  eqeltrid  2316  eqeltrdi  2320  ifcldadc  3632  ifcldcd  3640  intab  3952  disjiun  4078  iinexgm  4238  opexg  4314  tfisi  4679  nnpredcl  4715  imain  5403  fvmptd  5717  fvmptdf  5724  fvmptt  5728  elfvmptrab  5732  dffo3  5784  resfunexg  5864  f1oiso2  5957  riota2df  5982  riota5f  5987  ovmpodxf  6136  ovmpodf  6142  offval  6232  ofvalg  6234  offeq  6238  iunexg  6270  oprabexd  6278  fo1stresm  6313  fo2ndresm  6314  oprssdmm  6323  1stdm  6334  1stconst  6373  2ndconst  6374  cnvf1olem  6376  fo2ndf  6379  f1od2  6387  iunon  6436  tfrlemibacc  6478  tfrlemibfn  6480  tfr1onlembacc  6494  tfr1onlembfn  6496  tfrcllembacc  6507  tfrcllembfn  6509  tfrcl  6516  rdgon  6538  frec0g  6549  freccllem  6554  frecfcllem  6556  frecsuclem  6558  oacl  6614  omcl  6615  oeicl  6616  nntr2  6657  mptelixpg  6889  fidifsnen  7040  en2eqpr  7080  unfiin  7099  tpfidceq  7103  ssfirab  7109  fnfi  7114  relcnvfi  7119  fidcenumlemr  7133  elfi2  7150  supclti  7176  supubti  7177  suplubti  7178  supelti  7180  ordiso2  7213  djulclr  7227  djurclr  7228  djulcl  7229  djurcl  7230  djuss  7248  updjudhcoinlf  7258  updjudhcoinrg  7259  ctssdclemn0  7288  ctssdccl  7289  ctssdc  7291  enumctlemm  7292  nninfwlpoimlemg  7353  cardcl  7364  exmidontriimlem2  7415  exmidapne  7457  cc2lem  7463  cc3  7465  addclpi  7525  mulclpi  7526  addclnq  7573  mulclnq  7574  addclnq0  7649  mulclnq0  7650  nqpnq0nq  7651  elnp1st2nd  7674  prarloclemcalc  7700  distrlem1prl  7780  distrlem1pru  7781  ltexprlemopl  7799  ltexprlemopu  7801  ltexprlemfl  7807  ltexprlemrl  7808  ltexprlemfu  7809  ltexprlemru  7810  addcanprlemu  7813  recexprlemloc  7829  aptiprleml  7837  caucvgprprlemopl  7895  suplocexprlemex  7920  addclsr  7951  mulclsr  7952  recexgt0sr  7971  mulextsr1lem  7978  suplocsrlemb  8004  suplocsrlempr  8005  suplocsrlem  8006  axaddcl  8062  axaddrcl  8063  axmulcl  8064  axmulrcl  8065  axcaucvglemval  8095  subcl  8356  cru  8760  aprcl  8804  aptap  8808  divclap  8836  redivclap  8889  diveqap1bd  8994  lbinfcl  9107  cju  9119  nn1m1nn  9139  nnsub  9160  nnnn0addcl  9410  un0addcl  9413  peano2z  9493  peano2zm  9495  zaddcllemneg  9496  zaddcl  9497  nnaddm1cl  9519  nn0n0n1ge2  9528  zdivadd  9547  zdivmul  9548  suprzclex  9556  zneo  9559  peano5uzti  9566  supinfneg  9802  infsupneg  9803  qmulz  9830  qnegcl  9843  qapne  9846  qdivcl  9850  cnref1o  9858  xnegcl  10040  xltnegi  10043  xaddnemnf  10065  xaddnepnf  10066  xnegdi  10076  xnpcan  10080  xltadd1  10084  xposdif  10090  xleaddadd  10095  iccf1o  10212  ige3m2fz  10257  ige2m1fz1  10317  zssinfcl  10464  infssuzex  10465  infssuzcldc  10467  zsupssdc  10470  suprzcl2dc  10471  rebtwn2z  10486  flqcl  10505  flapcl  10507  ceilqcl  10542  intfracq  10554  modqcl  10560  mulqmod0  10564  modqdifz  10570  zmodcl  10578  modfzo0difsn  10629  modsumfzodifsn  10630  frec2uzzd  10634  frec2uzsucd  10635  frec2uzuzd  10636  frecuzrdgrrn  10642  frec2uzrdg  10643  frecuzrdgrcl  10644  frecuzrdgsuc  10648  frecuzrdgrclt  10649  frecuzrdgg  10650  frecuzrdgsuctlem  10657  fzofig  10666  iseqovex  10692  seq3val  10694  seqvalcd  10695  seqf  10698  seqovcd  10701  seq3clss  10705  seq3caopr3  10725  iseqf1olemnab  10735  iseqf1olemqk  10741  iseqf1olemjpcl  10742  iseqf1olemqpcl  10743  iseqf1olemfvp  10744  seq3f1olemqsumkj  10745  seq3f1olemqsum  10747  seq3f1oleml  10750  seq3f1o  10751  seqf1oglem2a  10752  seqf1oglem1  10753  seqf1oglem2  10754  seq3distr  10766  ser0f  10768  ser3le  10771  exp3vallem  10774  exp3val  10775  exp1  10779  expcl2lemap  10785  m1expcl2  10795  expaddzap  10817  sqcl  10834  nnsqcl  10843  qsqcl  10845  zesq  10892  facp1  10964  faccl  10969  facdiv  10972  bcval  10983  bcrpcl  10987  bcp1n  10995  bcpasc  11000  permnn  11005  hashennn  11014  hashcl  11015  lencl  11088  wrdexg  11095  elovmpowrd  11126  lswcl  11135  ccatcl  11141  ccatrn  11157  lswccatn0lsw  11159  ccatalpha  11161  s1cl  11169  swrdclg  11197  swrdwrdsymbg  11211  ccatswrd  11217  pfxval  11221  fnpfx  11224  pfxclg  11225  pfxwrdsymbg  11237  ccatpfx  11248  lenrevpfxcctswrd  11259  wrdind  11269  wrd2ind  11270  shftlem  11342  ovshftex  11345  shftf  11356  seq3shft  11364  cjth  11372  imval  11376  recl  11379  imcl  11380  crre  11383  remim  11386  reim0b  11388  cvg1nlemcau  11510  uzin2  11513  resqrexlem1arp  11531  resqrexlemp1rp  11532  resqrexlemglsq  11548  resqrexlemga  11549  resqrtcl  11555  abscl  11577  absrpclap  11587  nn0abscl  11611  fzomaxdiflem  11638  fzomaxdif  11639  maxabslemab  11732  maxcl  11736  zmaxcl  11750  minmax  11756  mincl  11757  xrmaxcl  11778  xrmaxaddlem  11786  xrminmax  11791  xrmincl  11792  xrmineqinf  11795  xrminrpcl  11800  reccn2ap  11839  climaddc1  11855  climmulc2  11857  climsubc1  11858  climsubc2  11859  climle  11860  climlec2  11867  climcvg1nlem  11875  sumrbdclem  11903  fsum3cvg  11904  summodclem3  11906  summodclem2a  11907  zsumdc  11910  fsumgcl  11912  fsum3  11913  isumss  11917  fisumss  11918  isumss2  11919  fsum3cvg2  11920  fsum3ser  11923  fsumcl2lem  11924  fsumcllem  11925  fsumadd  11932  sumsnf  11935  fsumsplitsn  11936  isumcl  11951  isummulc2  11952  isumrecl  11955  isumge0  11956  isumadd  11957  fsum2dlemstep  11960  fisumcom2  11964  mptfzshft  11968  fsumrev  11969  fsummulc2  11974  iserabs  12001  isumshft  12016  isumsplit  12017  isum1p  12018  isumrpcl  12020  isumle  12021  isumlessdc  12022  trireciplem  12026  expcnvap0  12028  expcnvre  12029  expcnv  12030  explecnv  12031  geolim  12037  geolim2  12038  geo2lim  12042  cvgratnnlemsumlt  12054  cvgratz  12058  mertenslemub  12060  mertenslemi1  12061  mertenslem2  12062  mertensabs  12063  prodf1f  12069  prodfdivap  12073  prodrbdclem  12097  fproddccvg  12098  prodmodclem3  12101  prodmodclem2a  12102  zproddc  12105  fprodseq  12109  fprodntrivap  12110  prodssdc  12115  fprodmul  12117  prodsnf  12118  fprodsplitdc  12122  fprodunsn  12130  fprodcl2lem  12131  fprodcllem  12132  fprodabs  12142  fprodrev  12145  fprod2dlemstep  12148  fprodcom2fi  12152  fprodsplitsn  12159  efcllemp  12184  ef0lem  12186  efcvgfsum  12193  reefcl  12194  ege2le3  12197  efcj  12199  efaddlem  12200  eftlcvg  12213  eftlcl  12214  reeftlcl  12215  eftlub  12216  efsep  12217  effsumlt  12218  efgt1p2  12221  efgt1p  12222  reeff1  12226  tanclap  12235  resincl  12246  recoscl  12247  retanclap  12248  eirraplem  12303  dvdsval2  12316  fsumdvds  12368  sqoddm1div8z  12412  bitsinv1lem  12487  gcdval  12495  gcdn0cl  12498  gcddvds  12499  divgcdnnr  12512  uzwodc  12573  nn0seqcvgd  12578  ialgrlem1st  12579  ialgrlemconst  12580  algrf  12582  algrp1  12583  eucalgf  12592  eucalglt  12594  lcmval  12600  lcmcllem  12604  lcmgcdlem  12614  cncongr2  12641  sqrt2irrlem  12698  oddpwdclemxy  12706  oddpwdclemdc  12710  qden1elz  12742  phicl2  12751  phimullem  12762  eulerthlemth  12769  prmdiv  12772  odzcllem  12780  pythagtriplem8  12810  pythagtriplem9  12811  pcval  12834  pczcl  12836  pcqcl  12844  dvdsprmpweqle  12875  pcaddlem  12877  pcmptcl  12880  pcmpt  12881  pockthlem  12894  pockthg  12895  zgz  12911  gznegcl  12913  gzcjcl  12914  gzaddcl  12915  gzmulcl  12916  gzabssqcl  12919  4sqlem5  12920  4sqlem4a  12929  mul4sqlem  12931  mul4sq  12932  4sqlemafi  12933  4sqlemffi  12934  4sqleminfi  12935  4sqexercise1  12936  4sqlem16  12944  4sqlem17  12945  ennnfonelemjn  12988  ennnfonelemg  12989  ennnfonelemp1  12992  ctinfomlemom  13013  ctiunctlemfo  13025  nninfdclemcl  13034  nninfdclemf  13035  nninfdclemp1  13036  setsex  13079  strsetsid  13080  strslfv3  13093  bassetsnn  13104  ressex  13113  ressbas2d  13116  strressid  13119  tgvalex  13311  ptex  13312  prdsex  13317  prdsval  13321  imasex  13353  imasival  13354  imasbas  13355  imasplusg  13356  imasmulr  13357  imasaddfn  13365  imasaddval  13366  imasaddf  13367  imasmulfn  13368  imasmulval  13369  imasmulf  13370  qusval  13371  qusex  13373  qusaddvallemg  13381  qusaddflemg  13382  qusaddval  13383  qusaddf  13384  qusmulval  13385  qusmulf  13386  mgm1  13418  gsumress  13443  gsumprval  13447  prdsplusgsgrpcl  13462  prdsplusgcl  13494  prdsidlem  13495  pwsmnd  13498  mhmex  13510  subsubm  13531  0subm  13532  mhmeql  13540  gsumwsubmcl  13544  gsumfzcl  13547  grpsubval  13594  grplinv  13598  pwsgrp  13659  qusgrp2  13665  mulgval  13674  mulgex  13675  mulgfng  13676  mulg1  13681  mulgnnp1  13682  mulgnnsubcl  13686  mulgnn0subcl  13687  mulgsubcl  13688  mulgnndir  13703  subgex  13728  subgsubcl  13737  issubgrpd  13743  subsubg  13749  nsgconj  13758  0nsg  13766  triv1nsgd  13770  eqgex  13773  eqger  13776  eqgcpbl  13780  ghmex  13807  ghmpreima  13818  ghmnsgpreima  13821  conjnmz  13831  gsumfzsubmcl  13890  mgpex  13903  rngmgpf  13915  qusrng  13936  mgpf  13989  qusring2  14044  opprex  14051  opprrng  14055  opprring  14057  dvdsrex  14077  opprunitd  14089  dvrvald  14113  dvrcl  14114  unitdvcl  14115  invrpropdg  14128  subsubrng  14193  subrgcrng  14204  subrgsubm  14213  subrgugrp  14219  subsubrg  14224  rnrhmsubrg  14231  aprcotr  14264  rmodislmod  14330  lssvsubcl  14345  islss3  14358  lspex  14374  ellspsn  14396  sraex  14425  rlmlmod  14443  lidlex  14452  rspex  14453  lidl0cl  14462  lidlacl  14463  lidlnegcl  14464  ridl0  14489  ridl1  14490  2idlelbas  14495  cnsubglem  14558  expghmap  14586  mulgrhm  14588  zrhex  14600  znbaslemnn  14618  psrval  14645  psrbagfi  14652  psrbasg  14653  mplsubgfilemm  14677  mplsubgfilemcl  14678  mplsubgfileminv  14679  mplgrpfi  14685  iunopn  14691  toponmax  14714  tgtop  14757  tgiun  14762  tgidm  14763  ntropn  14806  tgrest  14858  restopnb  14870  cnovex  14885  cnclima  14912  txvalex  14943  txtop  14949  tx1cn  14958  tx2cn  14959  txcnp  14960  txcnmpt  14962  txdis1cn  14967  cnmptcom  14987  imasnopn  14988  hmeocnv  14996  hmeores  15004  txhmeo  15008  txswaphmeo  15010  ispsmet  15012  xmetres  15071  metres  15072  blex  15076  xmeter  15125  xmetresbl  15129  mopntopon  15132  isxms2  15141  xmetxp  15196  xmettx  15199  txmetcnp  15207  qtopbasss  15210  qtopbas  15211  reopnap  15235  ioo2blex  15241  blssioo  15242  tgioo  15243  fsumcncntop  15256  expcn  15258  cncfval  15261  divccncfap  15279  cdivcncfap  15293  divcncfap  15303  maxcncf  15304  mincncf  15305  ivthdec  15333  hoverb  15337  limccnpcntop  15364  dvrecap  15402  elplyd  15430  ply1termlem  15431  ply1term  15432  plymullem1  15437  plyaddlem  15438  plymullem  15439  plycolemc  15447  plyco  15448  plycj  15450  plycn  15451  plyreres  15453  dvply1  15454  dvply2g  15455  pilem3  15472  tanrpcl  15526  cosordlem  15538  ioocosf1o  15543  rpcncxpcl  15591  rpcxpcl  15592  rpabscxpbnd  15629  rplogbcl  15635  sgmnncl  15677  mpodvdsmulf1o  15679  fsumdvdsmul  15680  mersenne  15686  perfectlem2  15689  lgslem1  15694  lgsval  15698  lgscllem  15701  lgsne0  15732  gausslemma2dlem4  15758  lgseisenlem1  15764  lgsquadlem1  15771  lgsquadlem2  15772  2sqlem3  15811  2sqlem8  15817  vtxex  15834  iedgex  15835  edgvalg  15875  edgopval  15877  edgstruct  15879  usgrausgrien  15982  ausgrumgrien  15983  ausgrusgrien  15984  vtxdgfif  16052  vtxdfifiun  16056  wlkex  16066  wlkelvv  16090  clwwlkccat  16138  djucllem  16219  012of  16416  2o01f  16417  nninfsellemeq  16440  qdencn  16455  cvgcmp2nlemabs  16460  trilpolemclim  16464  trilpolemisumle  16466  trilpolemeq1  16468  trilpolemlt1  16469  nconstwlpolemgt0  16492