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  3951  disjiun  4077  iinexgm  4237  opexg  4313  tfisi  4678  nnpredcl  4714  imain  5402  fvmptd  5714  fvmptdf  5721  fvmptt  5725  elfvmptrab  5729  dffo3  5781  resfunexg  5859  f1oiso2  5950  riota2df  5975  riota5f  5980  ovmpodxf  6129  ovmpodf  6135  offval  6224  ofvalg  6226  offeq  6230  iunexg  6262  oprabexd  6270  fo1stresm  6305  fo2ndresm  6306  oprssdmm  6315  1stdm  6326  1stconst  6365  2ndconst  6366  cnvf1olem  6368  fo2ndf  6371  f1od2  6379  iunon  6428  tfrlemibacc  6470  tfrlemibfn  6472  tfr1onlembacc  6486  tfr1onlembfn  6488  tfrcllembacc  6499  tfrcllembfn  6501  tfrcl  6508  rdgon  6530  frec0g  6541  freccllem  6546  frecfcllem  6548  frecsuclem  6550  oacl  6604  omcl  6605  oeicl  6606  nntr2  6647  mptelixpg  6879  fidifsnen  7028  en2eqpr  7065  unfiin  7084  tpfidceq  7088  ssfirab  7094  fnfi  7099  relcnvfi  7104  fidcenumlemr  7118  elfi2  7135  supclti  7161  supubti  7162  suplubti  7163  supelti  7165  ordiso2  7198  djulclr  7212  djurclr  7213  djulcl  7214  djurcl  7215  djuss  7233  updjudhcoinlf  7243  updjudhcoinrg  7244  ctssdclemn0  7273  ctssdccl  7274  ctssdc  7276  enumctlemm  7277  nninfwlpoimlemg  7338  cardcl  7349  exmidontriimlem2  7400  exmidapne  7442  cc2lem  7448  cc3  7450  addclpi  7510  mulclpi  7511  addclnq  7558  mulclnq  7559  addclnq0  7634  mulclnq0  7635  nqpnq0nq  7636  elnp1st2nd  7659  prarloclemcalc  7685  distrlem1prl  7765  distrlem1pru  7766  ltexprlemopl  7784  ltexprlemopu  7786  ltexprlemfl  7792  ltexprlemrl  7793  ltexprlemfu  7794  ltexprlemru  7795  addcanprlemu  7798  recexprlemloc  7814  aptiprleml  7822  caucvgprprlemopl  7880  suplocexprlemex  7905  addclsr  7936  mulclsr  7937  recexgt0sr  7956  mulextsr1lem  7963  suplocsrlemb  7989  suplocsrlempr  7990  suplocsrlem  7991  axaddcl  8047  axaddrcl  8048  axmulcl  8049  axmulrcl  8050  axcaucvglemval  8080  subcl  8341  cru  8745  aprcl  8789  aptap  8793  divclap  8821  redivclap  8874  diveqap1bd  8979  lbinfcl  9092  cju  9104  nn1m1nn  9124  nnsub  9145  nnnn0addcl  9395  un0addcl  9398  peano2z  9478  peano2zm  9480  zaddcllemneg  9481  zaddcl  9482  nnaddm1cl  9504  nn0n0n1ge2  9513  zdivadd  9532  zdivmul  9533  suprzclex  9541  zneo  9544  peano5uzti  9551  supinfneg  9786  infsupneg  9787  qmulz  9814  qnegcl  9827  qapne  9830  qdivcl  9834  cnref1o  9842  xnegcl  10024  xltnegi  10027  xaddnemnf  10049  xaddnepnf  10050  xnegdi  10060  xnpcan  10064  xltadd1  10068  xposdif  10074  xleaddadd  10079  iccf1o  10196  ige3m2fz  10241  ige2m1fz1  10301  zssinfcl  10447  infssuzex  10448  infssuzcldc  10450  zsupssdc  10453  suprzcl2dc  10454  rebtwn2z  10469  flqcl  10488  flapcl  10490  ceilqcl  10525  intfracq  10537  modqcl  10543  mulqmod0  10547  modqdifz  10553  zmodcl  10561  modfzo0difsn  10612  modsumfzodifsn  10613  frec2uzzd  10617  frec2uzsucd  10618  frec2uzuzd  10619  frecuzrdgrrn  10625  frec2uzrdg  10626  frecuzrdgrcl  10627  frecuzrdgsuc  10631  frecuzrdgrclt  10632  frecuzrdgg  10633  frecuzrdgsuctlem  10640  fzofig  10649  iseqovex  10675  seq3val  10677  seqvalcd  10678  seqf  10681  seqovcd  10684  seq3clss  10688  seq3caopr3  10708  iseqf1olemnab  10718  iseqf1olemqk  10724  iseqf1olemjpcl  10725  iseqf1olemqpcl  10726  iseqf1olemfvp  10727  seq3f1olemqsumkj  10728  seq3f1olemqsum  10730  seq3f1oleml  10733  seq3f1o  10734  seqf1oglem2a  10735  seqf1oglem1  10736  seqf1oglem2  10737  seq3distr  10749  ser0f  10751  ser3le  10754  exp3vallem  10757  exp3val  10758  exp1  10762  expcl2lemap  10768  m1expcl2  10778  expaddzap  10800  sqcl  10817  nnsqcl  10826  qsqcl  10828  zesq  10875  facp1  10947  faccl  10952  facdiv  10955  bcval  10966  bcrpcl  10970  bcp1n  10978  bcpasc  10983  permnn  10988  hashennn  10997  hashcl  10998  lencl  11070  wrdexg  11077  elovmpowrd  11108  lswcl  11117  ccatcl  11123  ccatrn  11139  lswccatn0lsw  11141  s1cl  11149  swrdclg  11177  swrdwrdsymbg  11191  ccatswrd  11197  pfxval  11201  fnpfx  11204  pfxclg  11205  pfxwrdsymbg  11217  ccatpfx  11228  lenrevpfxcctswrd  11239  wrdind  11249  wrd2ind  11250  shftlem  11322  ovshftex  11325  shftf  11336  seq3shft  11344  cjth  11352  imval  11356  recl  11359  imcl  11360  crre  11363  remim  11366  reim0b  11368  cvg1nlemcau  11490  uzin2  11493  resqrexlem1arp  11511  resqrexlemp1rp  11512  resqrexlemglsq  11528  resqrexlemga  11529  resqrtcl  11535  abscl  11557  absrpclap  11567  nn0abscl  11591  fzomaxdiflem  11618  fzomaxdif  11619  maxabslemab  11712  maxcl  11716  zmaxcl  11730  minmax  11736  mincl  11737  xrmaxcl  11758  xrmaxaddlem  11766  xrminmax  11771  xrmincl  11772  xrmineqinf  11775  xrminrpcl  11780  reccn2ap  11819  climaddc1  11835  climmulc2  11837  climsubc1  11838  climsubc2  11839  climle  11840  climlec2  11847  climcvg1nlem  11855  sumrbdclem  11883  fsum3cvg  11884  summodclem3  11886  summodclem2a  11887  zsumdc  11890  fsumgcl  11892  fsum3  11893  isumss  11897  fisumss  11898  isumss2  11899  fsum3cvg2  11900  fsum3ser  11903  fsumcl2lem  11904  fsumcllem  11905  fsumadd  11912  sumsnf  11915  fsumsplitsn  11916  isumcl  11931  isummulc2  11932  isumrecl  11935  isumge0  11936  isumadd  11937  fsum2dlemstep  11940  fisumcom2  11944  mptfzshft  11948  fsumrev  11949  fsummulc2  11954  iserabs  11981  isumshft  11996  isumsplit  11997  isum1p  11998  isumrpcl  12000  isumle  12001  isumlessdc  12002  trireciplem  12006  expcnvap0  12008  expcnvre  12009  expcnv  12010  explecnv  12011  geolim  12017  geolim2  12018  geo2lim  12022  cvgratnnlemsumlt  12034  cvgratz  12038  mertenslemub  12040  mertenslemi1  12041  mertenslem2  12042  mertensabs  12043  prodf1f  12049  prodfdivap  12053  prodrbdclem  12077  fproddccvg  12078  prodmodclem3  12081  prodmodclem2a  12082  zproddc  12085  fprodseq  12089  fprodntrivap  12090  prodssdc  12095  fprodmul  12097  prodsnf  12098  fprodsplitdc  12102  fprodunsn  12110  fprodcl2lem  12111  fprodcllem  12112  fprodabs  12122  fprodrev  12125  fprod2dlemstep  12128  fprodcom2fi  12132  fprodsplitsn  12139  efcllemp  12164  ef0lem  12166  efcvgfsum  12173  reefcl  12174  ege2le3  12177  efcj  12179  efaddlem  12180  eftlcvg  12193  eftlcl  12194  reeftlcl  12195  eftlub  12196  efsep  12197  effsumlt  12198  efgt1p2  12201  efgt1p  12202  reeff1  12206  tanclap  12215  resincl  12226  recoscl  12227  retanclap  12228  eirraplem  12283  dvdsval2  12296  fsumdvds  12348  sqoddm1div8z  12392  bitsinv1lem  12467  gcdval  12475  gcdn0cl  12478  gcddvds  12479  divgcdnnr  12492  uzwodc  12553  nn0seqcvgd  12558  ialgrlem1st  12559  ialgrlemconst  12560  algrf  12562  algrp1  12563  eucalgf  12572  eucalglt  12574  lcmval  12580  lcmcllem  12584  lcmgcdlem  12594  cncongr2  12621  sqrt2irrlem  12678  oddpwdclemxy  12686  oddpwdclemdc  12690  qden1elz  12722  phicl2  12731  phimullem  12742  eulerthlemth  12749  prmdiv  12752  odzcllem  12760  pythagtriplem8  12790  pythagtriplem9  12791  pcval  12814  pczcl  12816  pcqcl  12824  dvdsprmpweqle  12855  pcaddlem  12857  pcmptcl  12860  pcmpt  12861  pockthlem  12874  pockthg  12875  zgz  12891  gznegcl  12893  gzcjcl  12894  gzaddcl  12895  gzmulcl  12896  gzabssqcl  12899  4sqlem5  12900  4sqlem4a  12909  mul4sqlem  12911  mul4sq  12912  4sqlemafi  12913  4sqlemffi  12914  4sqleminfi  12915  4sqexercise1  12916  4sqlem16  12924  4sqlem17  12925  ennnfonelemjn  12968  ennnfonelemg  12969  ennnfonelemp1  12972  ctinfomlemom  12993  ctiunctlemfo  13005  nninfdclemcl  13014  nninfdclemf  13015  nninfdclemp1  13016  setsex  13059  strsetsid  13060  strslfv3  13073  bassetsnn  13084  ressex  13093  ressbas2d  13096  strressid  13099  tgvalex  13291  ptex  13292  prdsex  13297  prdsval  13301  imasex  13333  imasival  13334  imasbas  13335  imasplusg  13336  imasmulr  13337  imasaddfn  13345  imasaddval  13346  imasaddf  13347  imasmulfn  13348  imasmulval  13349  imasmulf  13350  qusval  13351  qusex  13353  qusaddvallemg  13361  qusaddflemg  13362  qusaddval  13363  qusaddf  13364  qusmulval  13365  qusmulf  13366  mgm1  13398  gsumress  13423  gsumprval  13427  prdsplusgsgrpcl  13442  prdsplusgcl  13474  prdsidlem  13475  pwsmnd  13478  mhmex  13490  subsubm  13511  0subm  13512  mhmeql  13520  gsumwsubmcl  13524  gsumfzcl  13527  grpsubval  13574  grplinv  13578  pwsgrp  13639  qusgrp2  13645  mulgval  13654  mulgex  13655  mulgfng  13656  mulg1  13661  mulgnnp1  13662  mulgnnsubcl  13666  mulgnn0subcl  13667  mulgsubcl  13668  mulgnndir  13683  subgex  13708  subgsubcl  13717  issubgrpd  13723  subsubg  13729  nsgconj  13738  0nsg  13746  triv1nsgd  13750  eqgex  13753  eqger  13756  eqgcpbl  13760  ghmex  13787  ghmpreima  13798  ghmnsgpreima  13801  conjnmz  13811  gsumfzsubmcl  13870  mgpex  13883  rngmgpf  13895  qusrng  13916  mgpf  13969  qusring2  14024  opprex  14031  opprrng  14035  opprring  14037  dvdsrex  14056  opprunitd  14068  dvrvald  14092  dvrcl  14093  unitdvcl  14094  invrpropdg  14107  subsubrng  14172  subrgcrng  14183  subrgsubm  14192  subrgugrp  14198  subsubrg  14203  rnrhmsubrg  14210  aprcotr  14243  rmodislmod  14309  lssvsubcl  14324  islss3  14337  lspex  14353  ellspsn  14375  sraex  14404  rlmlmod  14422  lidlex  14431  rspex  14432  lidl0cl  14441  lidlacl  14442  lidlnegcl  14443  ridl0  14468  ridl1  14469  2idlelbas  14474  cnsubglem  14537  expghmap  14565  mulgrhm  14567  zrhex  14579  znbaslemnn  14597  psrval  14624  psrbagfi  14631  psrbasg  14632  mplsubgfilemm  14656  mplsubgfilemcl  14657  mplsubgfileminv  14658  mplgrpfi  14664  iunopn  14670  toponmax  14693  tgtop  14736  tgiun  14741  tgidm  14742  ntropn  14785  tgrest  14837  restopnb  14849  cnovex  14864  cnclima  14891  txvalex  14922  txtop  14928  tx1cn  14937  tx2cn  14938  txcnp  14939  txcnmpt  14941  txdis1cn  14946  cnmptcom  14966  imasnopn  14967  hmeocnv  14975  hmeores  14983  txhmeo  14987  txswaphmeo  14989  ispsmet  14991  xmetres  15050  metres  15051  blex  15055  xmeter  15104  xmetresbl  15108  mopntopon  15111  isxms2  15120  xmetxp  15175  xmettx  15178  txmetcnp  15186  qtopbasss  15189  qtopbas  15190  reopnap  15214  ioo2blex  15220  blssioo  15221  tgioo  15222  fsumcncntop  15235  expcn  15237  cncfval  15240  divccncfap  15258  cdivcncfap  15272  divcncfap  15282  maxcncf  15283  mincncf  15284  ivthdec  15312  hoverb  15316  limccnpcntop  15343  dvrecap  15381  elplyd  15409  ply1termlem  15410  ply1term  15411  plymullem1  15416  plyaddlem  15417  plymullem  15418  plycolemc  15426  plyco  15427  plycj  15429  plycn  15430  plyreres  15432  dvply1  15433  dvply2g  15434  pilem3  15451  tanrpcl  15505  cosordlem  15517  ioocosf1o  15522  rpcncxpcl  15570  rpcxpcl  15571  rpabscxpbnd  15608  rplogbcl  15614  sgmnncl  15656  mpodvdsmulf1o  15658  fsumdvdsmul  15659  mersenne  15665  perfectlem2  15668  lgslem1  15673  lgsval  15677  lgscllem  15680  lgsne0  15711  gausslemma2dlem4  15737  lgseisenlem1  15743  lgsquadlem1  15750  lgsquadlem2  15751  2sqlem3  15790  2sqlem8  15796  vtxex  15813  iedgex  15814  edgvalg  15854  edgopval  15856  edgstruct  15858  usgrausgrien  15961  ausgrumgrien  15962  ausgrusgrien  15963  djucllem  16122  012of  16316  2o01f  16317  nninfsellemeq  16339  qdencn  16354  cvgcmp2nlemabs  16359  trilpolemclim  16363  trilpolemisumle  16365  trilpolemeq1  16367  trilpolemlt1  16368  nconstwlpolemgt0  16391