Theorem eqeltrd 2270

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

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

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 2175

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

This theorem is referenced by:  eqeltrrd  2271  3eltr4d  2277  eqeltrid  2280  eqeltrdi  2284  ifcldadc  3587  ifcldcd  3594  intab  3900  disjiun  4025  iinexgm  4184  opexg  4258  tfisi  4620  nnpredcl  4656  imain  5337  fvmptd  5639  fvmptdf  5646  fvmptt  5650  elfvmptrab  5654  dffo3  5706  resfunexg  5780  f1oiso2  5871  riota2df  5895  riota5f  5899  ovmpodxf  6045  ovmpodf  6051  offval  6140  ofvalg  6142  offeq  6146  iunexg  6173  oprabexd  6181  fo1stresm  6216  fo2ndresm  6217  oprssdmm  6226  1stdm  6237  1stconst  6276  2ndconst  6277  cnvf1olem  6279  fo2ndf  6282  f1od2  6290  iunon  6339  tfrlemibacc  6381  tfrlemibfn  6383  tfr1onlembacc  6397  tfr1onlembfn  6399  tfrcllembacc  6410  tfrcllembfn  6412  tfrcl  6419  rdgon  6441  frec0g  6452  freccllem  6457  frecfcllem  6459  frecsuclem  6461  oacl  6515  omcl  6516  oeicl  6517  nntr2  6558  mptelixpg  6790  fidifsnen  6928  en2eqpr  6965  unfiin  6984  ssfirab  6992  fnfi  6997  relcnvfi  7002  fidcenumlemr  7016  elfi2  7033  supclti  7059  supubti  7060  suplubti  7061  supelti  7063  ordiso2  7096  djulclr  7110  djurclr  7111  djulcl  7112  djurcl  7113  djuss  7131  updjudhcoinlf  7141  updjudhcoinrg  7142  ctssdclemn0  7171  ctssdccl  7172  ctssdc  7174  enumctlemm  7175  nninfwlpoimlemg  7236  cardcl  7243  exmidontriimlem2  7284  exmidapne  7322  cc2lem  7328  cc3  7330  addclpi  7389  mulclpi  7390  addclnq  7437  mulclnq  7438  addclnq0  7513  mulclnq0  7514  nqpnq0nq  7515  elnp1st2nd  7538  prarloclemcalc  7564  distrlem1prl  7644  distrlem1pru  7645  ltexprlemopl  7663  ltexprlemopu  7665  ltexprlemfl  7671  ltexprlemrl  7672  ltexprlemfu  7673  ltexprlemru  7674  addcanprlemu  7677  recexprlemloc  7693  aptiprleml  7701  caucvgprprlemopl  7759  suplocexprlemex  7784  addclsr  7815  mulclsr  7816  recexgt0sr  7835  mulextsr1lem  7842  suplocsrlemb  7868  suplocsrlempr  7869  suplocsrlem  7870  axaddcl  7926  axaddrcl  7927  axmulcl  7928  axmulrcl  7929  axcaucvglemval  7959  subcl  8220  cru  8623  aprcl  8667  aptap  8671  divclap  8699  redivclap  8752  diveqap1bd  8857  lbinfcl  8970  cju  8982  nn1m1nn  9002  nnsub  9023  nnnn0addcl  9273  un0addcl  9276  peano2z  9356  peano2zm  9358  zaddcllemneg  9359  zaddcl  9360  nnaddm1cl  9381  nn0n0n1ge2  9390  zdivadd  9409  zdivmul  9410  suprzclex  9418  zneo  9421  peano5uzti  9428  supinfneg  9663  infsupneg  9664  qmulz  9691  qnegcl  9704  qapne  9707  qdivcl  9711  cnref1o  9719  xnegcl  9901  xltnegi  9904  xaddnemnf  9926  xaddnepnf  9927  xnegdi  9937  xnpcan  9941  xltadd1  9945  xposdif  9951  xleaddadd  9956  iccf1o  10073  ige3m2fz  10118  ige2m1fz1  10178  rebtwn2z  10326  flqcl  10345  flapcl  10347  ceilqcl  10382  intfracq  10394  modqcl  10400  mulqmod0  10404  modqdifz  10410  zmodcl  10418  modfzo0difsn  10469  modsumfzodifsn  10470  frec2uzzd  10474  frec2uzsucd  10475  frec2uzuzd  10476  frecuzrdgrrn  10482  frec2uzrdg  10483  frecuzrdgrcl  10484  frecuzrdgsuc  10488  frecuzrdgrclt  10489  frecuzrdgg  10490  frecuzrdgsuctlem  10497  fzofig  10506  iseqovex  10532  seq3val  10534  seqvalcd  10535  seqf  10538  seqovcd  10541  seq3clss  10545  seq3caopr3  10565  iseqf1olemnab  10575  iseqf1olemqk  10581  iseqf1olemjpcl  10582  iseqf1olemqpcl  10583  iseqf1olemfvp  10584  seq3f1olemqsumkj  10585  seq3f1olemqsum  10587  seq3f1oleml  10590  seq3f1o  10591  seqf1oglem2a  10592  seqf1oglem1  10593  seqf1oglem2  10594  seq3distr  10606  ser0f  10608  ser3le  10611  exp3vallem  10614  exp3val  10615  exp1  10619  expcl2lemap  10625  m1expcl2  10635  expaddzap  10657  sqcl  10674  nnsqcl  10683  qsqcl  10685  zesq  10732  facp1  10804  faccl  10809  facdiv  10812  bcval  10823  bcrpcl  10827  bcp1n  10835  bcpasc  10840  permnn  10845  hashennn  10854  hashcl  10855  lencl  10921  wrdexg  10928  elovmpowrd  10958  shftlem  10963  ovshftex  10966  shftf  10977  seq3shft  10985  cjth  10993  imval  10997  recl  11000  imcl  11001  crre  11004  remim  11007  reim0b  11009  cvg1nlemcau  11131  uzin2  11134  resqrexlem1arp  11152  resqrexlemp1rp  11153  resqrexlemglsq  11169  resqrexlemga  11170  resqrtcl  11176  abscl  11198  absrpclap  11208  nn0abscl  11232  fzomaxdiflem  11259  fzomaxdif  11260  maxabslemab  11353  maxcl  11357  zmaxcl  11371  minmax  11376  mincl  11377  xrmaxcl  11398  xrmaxaddlem  11406  xrminmax  11411  xrmincl  11412  xrmineqinf  11415  xrminrpcl  11420  reccn2ap  11459  climaddc1  11475  climmulc2  11477  climsubc1  11478  climsubc2  11479  climle  11480  climlec2  11487  climcvg1nlem  11495  sumrbdclem  11523  fsum3cvg  11524  summodclem3  11526  summodclem2a  11527  zsumdc  11530  fsumgcl  11532  fsum3  11533  isumss  11537  fisumss  11538  isumss2  11539  fsum3cvg2  11540  fsum3ser  11543  fsumcl2lem  11544  fsumcllem  11545  fsumadd  11552  sumsnf  11555  fsumsplitsn  11556  isumcl  11571  isummulc2  11572  isumrecl  11575  isumge0  11576  isumadd  11577  fsum2dlemstep  11580  fisumcom2  11584  mptfzshft  11588  fsumrev  11589  fsummulc2  11594  iserabs  11621  isumshft  11636  isumsplit  11637  isum1p  11638  isumrpcl  11640  isumle  11641  isumlessdc  11642  trireciplem  11646  expcnvap0  11648  expcnvre  11649  expcnv  11650  explecnv  11651  geolim  11657  geolim2  11658  geo2lim  11662  cvgratnnlemsumlt  11674  cvgratz  11678  mertenslemub  11680  mertenslemi1  11681  mertenslem2  11682  mertensabs  11683  prodf1f  11689  prodfdivap  11693  prodrbdclem  11717  fproddccvg  11718  prodmodclem3  11721  prodmodclem2a  11722  zproddc  11725  fprodseq  11729  fprodntrivap  11730  prodssdc  11735  fprodmul  11737  prodsnf  11738  fprodsplitdc  11742  fprodunsn  11750  fprodcl2lem  11751  fprodcllem  11752  fprodabs  11762  fprodrev  11765  fprod2dlemstep  11768  fprodcom2fi  11772  fprodsplitsn  11779  efcllemp  11804  ef0lem  11806  efcvgfsum  11813  reefcl  11814  ege2le3  11817  efcj  11819  efaddlem  11820  eftlcvg  11833  eftlcl  11834  reeftlcl  11835  eftlub  11836  efsep  11837  effsumlt  11838  efgt1p2  11841  efgt1p  11842  reeff1  11846  tanclap  11855  resincl  11866  recoscl  11867  retanclap  11868  eirraplem  11923  dvdsval2  11936  sqoddm1div8z  12030  zssinfcl  12088  infssuzex  12089  infssuzcldc  12091  zsupssdc  12094  suprzcl2dc  12095  gcdval  12099  gcdn0cl  12102  gcddvds  12103  divgcdnnr  12116  uzwodc  12177  nn0seqcvgd  12182  ialgrlem1st  12183  ialgrlemconst  12184  algrf  12186  algrp1  12187  eucalgf  12196  eucalglt  12198  lcmval  12204  lcmcllem  12208  lcmgcdlem  12218  cncongr2  12245  sqrt2irrlem  12302  oddpwdclemxy  12310  oddpwdclemdc  12314  qden1elz  12346  phicl2  12355  phimullem  12366  eulerthlemth  12373  prmdiv  12376  odzcllem  12383  pythagtriplem8  12413  pythagtriplem9  12414  pcval  12437  pczcl  12439  pcqcl  12447  dvdsprmpweqle  12478  pcaddlem  12480  pcmptcl  12483  pcmpt  12484  pockthlem  12497  pockthg  12498  zgz  12514  gznegcl  12516  gzcjcl  12517  gzaddcl  12518  gzmulcl  12519  gzabssqcl  12522  4sqlem5  12523  4sqlem4a  12532  mul4sqlem  12534  mul4sq  12535  4sqlemafi  12536  4sqlemffi  12537  4sqleminfi  12538  4sqexercise1  12539  4sqlem16  12547  4sqlem17  12548  ennnfonelemjn  12562  ennnfonelemg  12563  ennnfonelemp1  12566  ctinfomlemom  12587  ctiunctlemfo  12599  nninfdclemcl  12608  nninfdclemf  12609  nninfdclemp1  12610  setsex  12653  strsetsid  12654  ressex  12686  ressbas2d  12689  strressid  12692  tgvalex  12877  ptex  12878  prdsex  12883  imasex  12891  imasival  12892  imasbas  12893  imasplusg  12894  imasmulr  12895  imasaddfn  12903  imasaddval  12904  imasaddf  12905  imasmulfn  12906  imasmulval  12907  imasmulf  12908  qusval  12909  qusex  12911  qusaddvallemg  12919  qusaddflemg  12920  qusaddval  12921  qusaddf  12922  qusmulval  12923  qusmulf  12924  mgm1  12956  gsumress  12981  gsumprval  12985  mhmex  13037  subsubm  13058  0subm  13059  mhmeql  13067  gsumwsubmcl  13071  gsumfzcl  13074  grpsubval  13121  grplinv  13125  qusgrp2  13186  mulgval  13195  mulgex  13196  mulgfng  13197  mulg1  13202  mulgnnp1  13203  mulgnnsubcl  13207  mulgnn0subcl  13208  mulgsubcl  13209  mulgnndir  13224  subgex  13249  subgsubcl  13258  issubgrpd  13264  subsubg  13270  nsgconj  13279  0nsg  13287  triv1nsgd  13291  eqgex  13294  eqger  13297  eqgcpbl  13301  ghmex  13328  ghmpreima  13339  ghmnsgpreima  13342  conjnmz  13352  gsumfzsubmcl  13411  mgpex  13424  rngmgpf  13436  qusrng  13457  mgpf  13510  qusring2  13565  opprex  13572  opprrng  13576  opprring  13578  dvdsrex  13597  opprunitd  13609  dvrvald  13633  dvrcl  13634  unitdvcl  13635  invrpropdg  13648  subsubrng  13713  subrgcrng  13724  subrgsubm  13733  subrgugrp  13739  subsubrg  13744  rnrhmsubrg  13751  aprcotr  13784  rmodislmod  13850  lssvsubcl  13865  islss3  13878  lspex  13894  ellspsn  13916  sraex  13945  rlmlmod  13963  lidlex  13972  rspex  13973  lidl0cl  13982  lidlacl  13983  lidlnegcl  13984  ridl0  14009  ridl1  14010  2idlelbas  14015  cnsubglem  14078  expghmap  14106  mulgrhm  14108  zrhex  14120  znbaslemnn  14138  psrval  14163  psrbasg  14170  iunopn  14181  toponmax  14204  tgtop  14247  tgiun  14252  tgidm  14253  ntropn  14296  tgrest  14348  restopnb  14360  cnovex  14375  cnclima  14402  txvalex  14433  txtop  14439  tx1cn  14448  tx2cn  14449  txcnp  14450  txcnmpt  14452  txdis1cn  14457  cnmptcom  14477  imasnopn  14478  hmeocnv  14486  hmeores  14494  txhmeo  14498  txswaphmeo  14500  ispsmet  14502  xmetres  14561  metres  14562  blex  14566  xmeter  14615  xmetresbl  14619  mopntopon  14622  isxms2  14631  xmetxp  14686  xmettx  14689  txmetcnp  14697  qtopbasss  14700  qtopbas  14701  reopnap  14725  ioo2blex  14731  blssioo  14732  tgioo  14733  fsumcncntop  14746  expcn  14748  cncfval  14751  divccncfap  14769  cdivcncfap  14783  divcncfap  14793  maxcncf  14794  mincncf  14795  ivthdec  14823  hoverb  14827  limccnpcntop  14854  dvrecap  14892  elplyd  14920  ply1termlem  14921  ply1term  14922  plymullem1  14927  plyaddlem  14928  plymullem  14929  plycolemc  14936  plyco  14937  plycj  14939  plycn  14940  plyreres  14942  dvply1  14943  pilem3  14959  tanrpcl  15013  cosordlem  15025  ioocosf1o  15030  rpcncxpcl  15078  rpcxpcl  15079  rpabscxpbnd  15114  rplogbcl  15119  lgslem1  15157  lgsval  15161  lgscllem  15164  lgsne0  15195  gausslemma2dlem4  15221  lgseisenlem1  15227  lgsquadlem1  15234  lgsquadlem2  15235  2sqlem3  15274  2sqlem8  15280  djucllem  15362  012of  15556  2o01f  15557  nninfsellemeq  15574  qdencn  15587  cvgcmp2nlemabs  15592  trilpolemclim  15596  trilpolemisumle  15598  trilpolemeq1  15600  trilpolemlt1  15601  nconstwlpolemgt0  15624