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  3633  ifcldcd  3641  intab  3955  disjiun  4081  iinexgm  4242  opexg  4318  tfisi  4683  nnpredcl  4719  opabssxpd  4760  imain  5409  fvmptd  5723  fvmptdf  5730  fvmptt  5734  elfvmptrab  5738  dffo3  5790  resfunexg  5870  f1oiso2  5963  riota2df  5988  riota5f  5993  ovmpodxf  6142  ovmpodf  6148  offval  6238  ofvalg  6240  offeq  6244  iunexg  6276  oprabexd  6284  fo1stresm  6319  fo2ndresm  6320  oprssdmm  6329  1stdm  6340  1stconst  6381  2ndconst  6382  cnvf1olem  6384  fo2ndf  6387  f1od2  6395  iunon  6445  tfrlemibacc  6487  tfrlemibfn  6489  tfr1onlembacc  6503  tfr1onlembfn  6505  tfrcllembacc  6516  tfrcllembfn  6518  tfrcl  6525  rdgon  6547  frec0g  6558  freccllem  6563  frecfcllem  6565  frecsuclem  6567  oacl  6623  omcl  6624  oeicl  6625  nntr2  6666  mptelixpg  6898  fidifsnen  7052  en2eqpr  7092  unfiin  7111  tpfidceq  7115  ssfirab  7121  fnfi  7126  relcnvfi  7131  fidcenumlemr  7145  elfi2  7162  supclti  7188  supubti  7189  suplubti  7190  supelti  7192  ordiso2  7225  djulclr  7239  djurclr  7240  djulcl  7241  djurcl  7242  djuss  7260  updjudhcoinlf  7270  updjudhcoinrg  7271  ctssdclemn0  7300  ctssdccl  7301  ctssdc  7303  enumctlemm  7304  nninfwlpoimlemg  7365  cardcl  7376  exmidontriimlem2  7427  exmidapne  7469  cc2lem  7475  cc3  7477  addclpi  7537  mulclpi  7538  addclnq  7585  mulclnq  7586  addclnq0  7661  mulclnq0  7662  nqpnq0nq  7663  elnp1st2nd  7686  prarloclemcalc  7712  distrlem1prl  7792  distrlem1pru  7793  ltexprlemopl  7811  ltexprlemopu  7813  ltexprlemfl  7819  ltexprlemrl  7820  ltexprlemfu  7821  ltexprlemru  7822  addcanprlemu  7825  recexprlemloc  7841  aptiprleml  7849  caucvgprprlemopl  7907  suplocexprlemex  7932  addclsr  7963  mulclsr  7964  recexgt0sr  7983  mulextsr1lem  7990  suplocsrlemb  8016  suplocsrlempr  8017  suplocsrlem  8018  axaddcl  8074  axaddrcl  8075  axmulcl  8076  axmulrcl  8077  axcaucvglemval  8107  subcl  8368  cru  8772  aprcl  8816  aptap  8820  divclap  8848  redivclap  8901  diveqap1bd  9006  lbinfcl  9119  cju  9131  nn1m1nn  9151  nnsub  9172  nnnn0addcl  9422  un0addcl  9425  peano2z  9505  peano2zm  9507  zaddcllemneg  9508  zaddcl  9509  nnaddm1cl  9531  nn0n0n1ge2  9540  zdivadd  9559  zdivmul  9560  suprzclex  9568  zneo  9571  peano5uzti  9578  supinfneg  9819  infsupneg  9820  qmulz  9847  qnegcl  9860  qapne  9863  qdivcl  9867  cnref1o  9875  xnegcl  10057  xltnegi  10060  xaddnemnf  10082  xaddnepnf  10083  xnegdi  10093  xnpcan  10097  xltadd1  10101  xposdif  10107  xleaddadd  10112  iccf1o  10229  ige3m2fz  10274  ige2m1fz1  10334  zssinfcl  10482  infssuzex  10483  infssuzcldc  10485  zsupssdc  10488  suprzcl2dc  10489  rebtwn2z  10504  flqcl  10523  flapcl  10525  ceilqcl  10560  intfracq  10572  modqcl  10578  mulqmod0  10582  modqdifz  10588  zmodcl  10596  modfzo0difsn  10647  modsumfzodifsn  10648  frec2uzzd  10652  frec2uzsucd  10653  frec2uzuzd  10654  frecuzrdgrrn  10660  frec2uzrdg  10661  frecuzrdgrcl  10662  frecuzrdgsuc  10666  frecuzrdgrclt  10667  frecuzrdgg  10668  frecuzrdgsuctlem  10675  fzofig  10684  iseqovex  10710  seq3val  10712  seqvalcd  10713  seqf  10716  seqovcd  10719  seq3clss  10723  seq3caopr3  10743  iseqf1olemnab  10753  iseqf1olemqk  10759  iseqf1olemjpcl  10760  iseqf1olemqpcl  10761  iseqf1olemfvp  10762  seq3f1olemqsumkj  10763  seq3f1olemqsum  10765  seq3f1oleml  10768  seq3f1o  10769  seqf1oglem2a  10770  seqf1oglem1  10771  seqf1oglem2  10772  seq3distr  10784  ser0f  10786  ser3le  10789  exp3vallem  10792  exp3val  10793  exp1  10797  expcl2lemap  10803  m1expcl2  10813  expaddzap  10835  sqcl  10852  nnsqcl  10861  qsqcl  10863  zesq  10910  facp1  10982  faccl  10987  facdiv  10990  bcval  11001  bcrpcl  11005  bcp1n  11013  bcpasc  11018  permnn  11023  hashennn  11032  hashcl  11033  lencl  11107  wrdexg  11114  elovmpowrd  11145  lswcl  11154  ccatcl  11160  ccatrn  11176  lswccatn0lsw  11178  ccatalpha  11180  s1cl  11188  swrdclg  11221  swrdwrdsymbg  11235  ccatswrd  11241  pfxval  11245  fnpfx  11248  pfxclg  11249  pfxwrdsymbg  11261  ccatpfx  11272  lenrevpfxcctswrd  11283  wrdind  11293  wrd2ind  11294  shftlem  11367  ovshftex  11370  shftf  11381  seq3shft  11389  cjth  11397  imval  11401  recl  11404  imcl  11405  crre  11408  remim  11411  reim0b  11413  cvg1nlemcau  11535  uzin2  11538  resqrexlem1arp  11556  resqrexlemp1rp  11557  resqrexlemglsq  11573  resqrexlemga  11574  resqrtcl  11580  abscl  11602  absrpclap  11612  nn0abscl  11636  fzomaxdiflem  11663  fzomaxdif  11664  maxabslemab  11757  maxcl  11761  zmaxcl  11775  minmax  11781  mincl  11782  xrmaxcl  11803  xrmaxaddlem  11811  xrminmax  11816  xrmincl  11817  xrmineqinf  11820  xrminrpcl  11825  reccn2ap  11864  climaddc1  11880  climmulc2  11882  climsubc1  11883  climsubc2  11884  climle  11885  climlec2  11892  climcvg1nlem  11900  sumrbdclem  11928  fsum3cvg  11929  summodclem3  11931  summodclem2a  11932  zsumdc  11935  fsumgcl  11937  fsum3  11938  isumss  11942  fisumss  11943  isumss2  11944  fsum3cvg2  11945  fsum3ser  11948  fsumcl2lem  11949  fsumcllem  11950  fsumadd  11957  sumsnf  11960  fsumsplitsn  11961  isumcl  11976  isummulc2  11977  isumrecl  11980  isumge0  11981  isumadd  11982  fsum2dlemstep  11985  fisumcom2  11989  mptfzshft  11993  fsumrev  11994  fsummulc2  11999  iserabs  12026  isumshft  12041  isumsplit  12042  isum1p  12043  isumrpcl  12045  isumle  12046  isumlessdc  12047  trireciplem  12051  expcnvap0  12053  expcnvre  12054  expcnv  12055  explecnv  12056  geolim  12062  geolim2  12063  geo2lim  12067  cvgratnnlemsumlt  12079  cvgratz  12083  mertenslemub  12085  mertenslemi1  12086  mertenslem2  12087  mertensabs  12088  prodf1f  12094  prodfdivap  12098  prodrbdclem  12122  fproddccvg  12123  prodmodclem3  12126  prodmodclem2a  12127  zproddc  12130  fprodseq  12134  fprodntrivap  12135  prodssdc  12140  fprodmul  12142  prodsnf  12143  fprodsplitdc  12147  fprodunsn  12155  fprodcl2lem  12156  fprodcllem  12157  fprodabs  12167  fprodrev  12170  fprod2dlemstep  12173  fprodcom2fi  12177  fprodsplitsn  12184  efcllemp  12209  ef0lem  12211  efcvgfsum  12218  reefcl  12219  ege2le3  12222  efcj  12224  efaddlem  12225  eftlcvg  12238  eftlcl  12239  reeftlcl  12240  eftlub  12241  efsep  12242  effsumlt  12243  efgt1p2  12246  efgt1p  12247  reeff1  12251  tanclap  12260  resincl  12271  recoscl  12272  retanclap  12273  eirraplem  12328  dvdsval2  12341  fsumdvds  12393  sqoddm1div8z  12437  bitsinv1lem  12512  gcdval  12520  gcdn0cl  12523  gcddvds  12524  divgcdnnr  12537  uzwodc  12598  nn0seqcvgd  12603  ialgrlem1st  12604  ialgrlemconst  12605  algrf  12607  algrp1  12608  eucalgf  12617  eucalglt  12619  lcmval  12625  lcmcllem  12629  lcmgcdlem  12639  cncongr2  12666  sqrt2irrlem  12723  oddpwdclemxy  12731  oddpwdclemdc  12735  qden1elz  12767  phicl2  12776  phimullem  12787  eulerthlemth  12794  prmdiv  12797  odzcllem  12805  pythagtriplem8  12835  pythagtriplem9  12836  pcval  12859  pczcl  12861  pcqcl  12869  dvdsprmpweqle  12900  pcaddlem  12902  pcmptcl  12905  pcmpt  12906  pockthlem  12919  pockthg  12920  zgz  12936  gznegcl  12938  gzcjcl  12939  gzaddcl  12940  gzmulcl  12941  gzabssqcl  12944  4sqlem5  12945  4sqlem4a  12954  mul4sqlem  12956  mul4sq  12957  4sqlemafi  12958  4sqlemffi  12959  4sqleminfi  12960  4sqexercise1  12961  4sqlem16  12969  4sqlem17  12970  ennnfonelemjn  13013  ennnfonelemg  13014  ennnfonelemp1  13017  ctinfomlemom  13038  ctiunctlemfo  13050  nninfdclemcl  13059  nninfdclemf  13060  nninfdclemp1  13061  setsex  13104  strsetsid  13105  strslfv3  13118  bassetsnn  13129  ressex  13138  ressbas2d  13141  strressid  13144  tgvalex  13336  ptex  13337  prdsex  13342  prdsval  13346  imasex  13378  imasival  13379  imasbas  13380  imasplusg  13381  imasmulr  13382  imasaddfn  13390  imasaddval  13391  imasaddf  13392  imasmulfn  13393  imasmulval  13394  imasmulf  13395  qusval  13396  qusex  13398  qusaddvallemg  13406  qusaddflemg  13407  qusaddval  13408  qusaddf  13409  qusmulval  13410  qusmulf  13411  mgm1  13443  gsumress  13468  gsumprval  13472  prdsplusgsgrpcl  13487  prdsplusgcl  13519  prdsidlem  13520  pwsmnd  13523  mhmex  13535  subsubm  13556  0subm  13557  mhmeql  13565  gsumwsubmcl  13569  gsumfzcl  13572  grpsubval  13619  grplinv  13623  pwsgrp  13684  qusgrp2  13690  mulgval  13699  mulgex  13700  mulgfng  13701  mulg1  13706  mulgnnp1  13707  mulgnnsubcl  13711  mulgnn0subcl  13712  mulgsubcl  13713  mulgnndir  13728  subgex  13753  subgsubcl  13762  issubgrpd  13768  subsubg  13774  nsgconj  13783  0nsg  13791  triv1nsgd  13795  eqgex  13798  eqger  13801  eqgcpbl  13805  ghmex  13832  ghmpreima  13843  ghmnsgpreima  13846  conjnmz  13856  gsumfzsubmcl  13915  mgpex  13928  rngmgpf  13940  qusrng  13961  mgpf  14014  qusring2  14069  opprex  14076  opprrng  14080  opprring  14082  dvdsrex  14102  opprunitd  14114  dvrvald  14138  dvrcl  14139  unitdvcl  14140  invrpropdg  14153  subsubrng  14218  subrgcrng  14229  subrgsubm  14238  subrgugrp  14244  subsubrg  14249  rnrhmsubrg  14256  aprcotr  14289  rmodislmod  14355  lssvsubcl  14370  islss3  14383  lspex  14399  ellspsn  14421  sraex  14450  rlmlmod  14468  lidlex  14477  rspex  14478  lidl0cl  14487  lidlacl  14488  lidlnegcl  14489  ridl0  14514  ridl1  14515  2idlelbas  14520  cnsubglem  14583  expghmap  14611  mulgrhm  14613  zrhex  14625  znbaslemnn  14643  psrval  14670  psrbagfi  14677  psrbasg  14678  mplsubgfilemm  14702  mplsubgfilemcl  14703  mplsubgfileminv  14704  mplgrpfi  14710  iunopn  14716  toponmax  14739  tgtop  14782  tgiun  14787  tgidm  14788  ntropn  14831  tgrest  14883  restopnb  14895  cnovex  14910  cnclima  14937  txvalex  14968  txtop  14974  tx1cn  14983  tx2cn  14984  txcnp  14985  txcnmpt  14987  txdis1cn  14992  cnmptcom  15012  imasnopn  15013  hmeocnv  15021  hmeores  15029  txhmeo  15033  txswaphmeo  15035  ispsmet  15037  xmetres  15096  metres  15097  blex  15101  xmeter  15150  xmetresbl  15154  mopntopon  15157  isxms2  15166  xmetxp  15221  xmettx  15224  txmetcnp  15232  qtopbasss  15235  qtopbas  15236  reopnap  15260  ioo2blex  15266  blssioo  15267  tgioo  15268  fsumcncntop  15281  expcn  15283  cncfval  15286  divccncfap  15304  cdivcncfap  15318  divcncfap  15328  maxcncf  15329  mincncf  15330  ivthdec  15358  hoverb  15362  limccnpcntop  15389  dvrecap  15427  elplyd  15455  ply1termlem  15456  ply1term  15457  plymullem1  15462  plyaddlem  15463  plymullem  15464  plycolemc  15472  plyco  15473  plycj  15475  plycn  15476  plyreres  15478  dvply1  15479  dvply2g  15480  pilem3  15497  tanrpcl  15551  cosordlem  15563  ioocosf1o  15568  rpcncxpcl  15616  rpcxpcl  15617  rpabscxpbnd  15654  rplogbcl  15660  sgmnncl  15702  mpodvdsmulf1o  15704  fsumdvdsmul  15705  mersenne  15711  perfectlem2  15714  lgslem1  15719  lgsval  15723  lgscllem  15726  lgsne0  15757  gausslemma2dlem4  15783  lgseisenlem1  15789  lgsquadlem1  15796  lgsquadlem2  15797  2sqlem3  15836  2sqlem8  15842  vtxex  15859  iedgex  15860  edgvalg  15900  edgopval  15903  edgstruct  15905  usgrausgrien  16008  ausgrumgrien  16009  ausgrusgrien  16010  uspgr1ewopdc  16083  usgr2v1e2w  16085  vtxdgfif  16099  vtxdfifiun  16103  1loopgrvd2fi  16111  1loopgrvd0fi  16112  1hevtxdg0fi  16113  wlkex  16122  wlkelvv  16146  clwwlkccat  16196  clwwlknonex2lem1  16232  clwwlknonex2lem2  16233  clwwlknonex2  16234  djucllem  16332  012of  16528  2o01f  16529  nninfsellemeq  16552  qdencn  16567  cvgcmp2nlemabs  16572  trilpolemclim  16576  trilpolemisumle  16578  trilpolemeq1  16580  trilpolemlt1  16581  nconstwlpolemgt0  16604