Theorem eqeltrd 2315

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 2307	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))
4	1, 3	mpbird 167	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:  eqeltrrd  2316  3eltr4d  2322  eqeltrid  2325  eqeltrdi  2329  ifcldadc  3670  ifcldcd  3678  intab  3999  disjiun  4125  iinexgm  4290  opexg  4368  tfisi  4734  nnpredcl  4770  opabssxpd  4811  imain  5463  fvmptd  5786  fvmptdf  5793  fvmptt  5797  elfvmptrab  5802  dffo3  5855  resfunexg  5936  f1oiso2  6033  riota2df  6060  riota5f  6065  ovmpodxf  6214  ovmpodf  6220  offval  6310  ofvalg  6312  offeq  6316  iunexg  6348  oprabexd  6360  fo1stresm  6395  fo2ndresm  6396  oprssdmm  6405  1stdm  6416  1stconst  6457  2ndconst  6458  cnvf1olem  6460  fo2ndf  6463  f1od2  6471  iunon  6555  tfrlemibacc  6597  tfrlemibfn  6599  tfr1onlembacc  6613  tfr1onlembfn  6615  tfrcllembacc  6626  tfrcllembfn  6628  tfrcl  6635  rdgon  6657  frec0g  6668  freccllem  6673  frecfcllem  6675  frecsuclem  6677  oacl  6733  omcl  6734  oeicl  6735  nntr2  6776  mptelixpg  7016  fidifsnen  7172  en2eqpr  7214  unfiin  7233  tpfidceq  7237  ssfirab  7244  fnfi  7250  relcnvfi  7255  fidcenumlemr  7272  snopfsuppdc  7299  fsuppcorn  7301  elfi2  7306  supclti  7339  supubti  7340  suplubti  7341  supelti  7343  ordiso2  7376  djulclr  7390  djurclr  7391  djulcl  7392  djurcl  7393  djuss  7411  updjudhcoinlf  7421  updjudhcoinrg  7422  ctssdclemn0  7451  ctssdccl  7452  ctssdc  7454  enumctlemm  7455  nninfwlpoimlemg  7516  cardcl  7527  exmidontriimlem2  7579  exmidapne  7627  cc2lem  7633  cc3  7635  addclpi  7695  mulclpi  7696  addclnq  7743  mulclnq  7744  addclnq0  7819  mulclnq0  7820  nqpnq0nq  7821  elnp1st2nd  7844  prarloclemcalc  7870  distrlem1prl  7950  distrlem1pru  7951  ltexprlemopl  7969  ltexprlemopu  7971  ltexprlemfl  7977  ltexprlemrl  7978  ltexprlemfu  7979  ltexprlemru  7980  addcanprlemu  7983  recexprlemloc  7999  aptiprleml  8007  caucvgprprlemopl  8065  suplocexprlemex  8090  addclsr  8121  mulclsr  8122  recexgt0sr  8141  mulextsr1lem  8148  suplocsrlemb  8174  suplocsrlempr  8175  suplocsrlem  8176  axaddcl  8232  axaddrcl  8233  axmulcl  8234  axmulrcl  8235  axcaucvglemval  8265  subcl  8527  cru  8933  aprcl  8977  aptap  8981  divclap  9011  redivclap  9064  diveqap1bd  9169  lbinfcl  9282  cju  9294  nn1m1nn  9325  nnsub  9346  nnnn0addcl  9598  un0addcl  9601  peano2z  9685  peano2zm  9687  zaddcllemneg  9688  zaddcl  9689  nnaddm1cl  9711  nn0n0n1ge2  9720  zdivadd  9740  zdivmul  9741  suprzclex  9749  zneo  9752  peano5uzti  9759  supinfneg  10005  infsupneg  10006  qmulz  10033  qnegcl  10046  qapne  10049  qdivcl  10053  cnref1o  10062  xnegcl  10245  xltnegi  10248  xaddnemnf  10270  xaddnepnf  10271  xnegdi  10281  xnpcan  10285  xltadd1  10289  xposdif  10295  xleaddadd  10300  iccf1o  10418  ige3m2fz  10465  ige2m1fz1  10527  zssinfcl  10676  infssuzex  10677  infssuzcldc  10679  zsupssdc  10684  suprzcl2dc  10685  rebtwn2z  10700  flqcl  10719  flapclz  10721  ceilqcl  10760  intfracq  10772  modqcl  10778  mulqmod0  10782  modqdifz  10788  zmodcl  10796  modfzo0difsn  10847  modsumfzodifsn  10848  frec2uzzd  10852  frec2uzsucd  10853  frec2uzuzd  10854  frecuzrdgrrn  10860  frec2uzrdg  10861  frecuzrdgrcl  10862  frecuzrdgsuc  10866  frecuzrdgrclt  10867  frecuzrdgg  10868  frecuzrdgsuctlem  10875  fzofig  10884  iseqovex  10910  seq3val  10912  seqvalcd  10913  seqf  10916  seqovcd  10919  seq3clss  10923  seq3caopr3  10943  iseqf1olemnab  10953  iseqf1olemqk  10959  iseqf1olemjpcl  10960  iseqf1olemqpcl  10961  iseqf1olemfvp  10962  seq3f1olemqsumkj  10963  seq3f1olemqsum  10965  seq3f1oleml  10968  seq3f1o  10969  seqf1oglem2a  10970  seqf1oglem1  10971  seqf1oglem2  10972  seq3distr  10984  ser0f  10986  ser3le  10989  exp3vallem  10992  exp3val  10993  exp1  10997  expcl2lemap  11003  m1expcl2  11013  expaddzap  11035  sqcl  11052  nnsqcl  11061  qsqcl  11063  zesq  11111  facp1  11184  faccl  11189  facdiv  11192  bcval  11203  bcrpcl  11207  bcp1n  11215  bcpasc  11220  permnn  11226  hashennn  11235  hashcl  11236  hashf1  11303  lencl  11324  wrdexg  11331  elovmpowrd  11362  lswcl  11371  ccatcl  11377  ccatrn  11393  lswccatn0lsw  11395  ccatalpha  11397  s1cl  11405  swrdclg  11438  swrdwrdsymbg  11452  ccatswrd  11458  pfxval  11462  fnpfx  11465  pfxclg  11466  pfxwrdsymbg  11478  ccatpfx  11489  lenrevpfxcctswrd  11500  wrdind  11510  wrd2ind  11511  shftlem  11597  ovshftex  11600  shftf  11611  seq3shft  11619  cjth  11627  imval  11631  recl  11634  imcl  11635  crre  11638  remim  11641  reim0b  11643  cvg1nlemcau  11766  uzin2  11769  resqrexlem1arp  11787  resqrexlemp1rp  11788  resqrexlemglsq  11804  resqrexlemga  11805  resqrtcl  11811  abscl  11833  absrpclap  11843  qabscl  11859  nn0abscl  11868  fzomaxdiflem  11895  fzomaxdif  11896  maxabslemab  11989  maxcl  11993  zmaxcl  12007  minmax  12014  mincl  12015  zmincl  12023  xrmaxcl  12037  xrmaxaddlem  12045  xrminmax  12050  xrmincl  12051  xrmineqinf  12054  xrminrpcl  12059  reccn2ap  12098  climaddc1  12114  climmulc2  12116  climsubc1  12117  climsubc2  12118  climle  12119  climlec2  12126  climcvg1nlem  12134  sumrbdclem  12163  fsum3cvg  12164  summodclem3  12166  summodclem2a  12167  zsumdc  12170  fsumgcl  12172  fsum3  12173  isumss  12177  fisumss  12178  isumss2  12179  fsum3cvg2  12180  fsum3ser  12183  fsumcl2lem  12184  fsumcllem  12185  fsumadd  12192  sumsnf  12195  fsumsplitsn  12196  isumcl  12211  isummulc2  12212  isumrecl  12215  isumge0  12216  isumadd  12217  fsum2dlemstep  12220  fisumcom2  12224  mptfzshft  12228  fsumrev  12229  fsummulc2  12234  iserabs  12261  isumshft  12276  isumsplit  12277  isum1p  12278  isumrpcl  12280  isumle  12281  isumlessdc  12282  trireciplem  12286  expcnvap0  12288  expcnvre  12289  expcnv  12290  explecnv  12291  geolim  12297  geolim2  12298  geo2lim  12302  cvgratnnlemsumlt  12314  cvgratz  12318  mertenslemub  12320  mertenslemi1  12321  mertenslem2  12322  mertensabs  12323  prodf1f  12329  prodfdivap  12333  prodrbdclem  12357  fproddccvg  12358  prodmodclem3  12361  prodmodclem2a  12362  zproddc  12365  fprodseq  12369  fprodntrivap  12370  prodssdc  12375  fprodmul  12377  prodsnf  12378  fprodsplitdc  12382  fprodunsn  12390  fprodcl2lem  12391  fprodcllem  12392  fprodabs  12402  fprodrev  12405  fprod2dlemstep  12408  fprodcom2fi  12412  fprodsplitsn  12419  efcllemp  12444  ef0lem  12446  efcvgfsum  12453  reefcl  12454  ege2le3  12457  efcj  12459  efaddlem  12460  eftlcvg  12473  eftlcl  12474  reeftlcl  12475  eftlub  12476  efsep  12477  effsumlt  12478  efgt1p2  12481  efgt1p  12482  reeff1  12486  tanclap  12495  resincl  12506  recoscl  12507  retanclap  12508  eirraplem  12563  dvdsval2  12576  fsumdvds  12628  sqoddm1div8z  12672  bitsinv1lem  12747  gcdval  12755  gcdn0cl  12758  gcddvds  12759  divgcdnnr  12772  uzwodc  12833  nn0seqcvgd  12838  ialgrlem1st  12839  ialgrlemconst  12840  algrf  12842  algrp1  12843  eucalgf  12852  eucalglt  12854  lcmval  12860  lcmcllem  12864  lcmgcdlem  12874  cncongr2  12901  sqrt2irrlem  12959  nnmaxpwlemxy  12967  nnmaxpwlemparts  12971  qden1elz  13004  nn0sqdcq  13007  sqrtrirr  13008  phicl2  13015  phimullem  13026  eulerthlemth  13033  prmdiv  13036  odzcllem  13044  pythagtriplem8  13074  pythagtriplem9  13075  pcval  13098  pczcl  13100  pcqcl  13108  dvdsprmpweqle  13139  pcaddlem  13141  pcmptcl  13144  pcmpt  13145  pockthlem  13158  pockthg  13159  zgz  13175  gznegcl  13177  gzcjcl  13178  gzaddcl  13179  gzmulcl  13180  gzabssqcl  13183  4sqlem5  13184  4sqlem4a  13193  mul4sqlem  13195  mul4sq  13196  4sqlemafi  13197  4sqlemffi  13198  4sqleminfi  13199  4sqexercise1  13200  4sqlem16  13208  4sqlem17  13209  ballotfilemfelz  13282  ballotfilemiex  13296  ballotfilemsdom  13307  ballotfilemgval  13319  ennnfonelemjn  13345  ennnfonelemg  13346  ennnfonelemp1  13349  ctinfomlemom  13370  ctiunctlemfo  13382  nninfdclemcl  13391  nninfdclemf  13392  nninfdclemp1  13393  setsex  13436  strsetsid  13437  strslfv3  13450  bassetsnn  13461  ressex  13471  ressbas2d  13475  strressid  13478  tgvalex  13670  ptex  13671  imasex  13679  imasival  13680  imasbas  13681  imasplusg  13682  imasmulr  13683  imasaddfn  13691  imasaddval  13692  imasaddf  13693  imasmulfn  13694  imasmulval  13695  imasmulf  13696  qusval  13697  qusex  13699  qusaddvallemg  13707  qusaddflemg  13708  qusaddval  13709  qusaddf  13710  qusmulval  13711  qusmulf  13712  mgm1  13743  gzsumress  13765  mhmex  13822  subsubm  13843  0subm  13844  mhmeql  13852  gzsumwsubmcl  13854  gzsumcl  13857  grpsubval  13904  grplinv  13908  qusgrp2  13969  mulgval  13978  mulgex  13979  mulgfng  13980  mulg1  13985  mulgnnp1  13986  mulgnnsubcl  13990  mulgnn0subcl  13991  mulgsubcl  13992  mulgnndir  14007  subgex  14032  subgsubcl  14041  issubgrpd  14047  subsubg  14053  nsgconj  14062  0nsg  14070  triv1nsgd  14074  eqgex  14077  eqger  14080  eqgcpbl  14084  ghmex  14111  ghmpreima  14122  ghmnsgpreima  14125  conjnmz  14135  cntzex  14144  cntrsubgnsg  14169  gzsumsubmcl  14226  gzsumsplit0  14232  gsumvalfi  14236  gsumsncmn  14240  gsumclfi  14243  gsumsubmclfi  14247  prdsex  14256  prdsval  14257  prdsplusgsgrpcl  14274  prdsplusgcl  14276  prdsidlem  14277  pwsmnd  14296  pwsgrp  14298  mgpex  14307  rngmgpf  14320  qusrng  14341  mgpf  14399  qusring2  14455  opprex  14462  opprrng  14466  opprring  14468  dvdsrex  14489  opprunitd  14501  dvrvald  14525  dvrcl  14526  unitdvcl  14527  invrpropdg  14540  subsubrng  14606  subrgcrng  14617  subrgsubm  14626  subrgugrp  14632  subsubrg  14637  rnrhmsubrg  14644  aprcotr  14681  aprnzr  14683  aprlring  14684  rmodislmod  14772  lssvsubcl  14787  islss3  14800  lspex  14816  ellspsn  14838  sraex  14867  rlmlmod  14885  lidlex  14894  rspex  14895  lidl0cl  14904  lidlacl  14905  lidlnegcl  14906  ridl0  14931  ridl1  14932  2idlelbas  14937  cnsubglem  15000  expghmap  15026  mulgrhm  15028  zrhex  15040  znbaslemnn  15058  asplss  15100  aspsubrg  15102  psrval  15134  psrbagfi  15143  psrbagcon  15146  psrbasg  15150  mplsubgfilemm  15180  mplsubgfilemcl  15181  mplsubgfileminv  15182  mplgrpfi  15188  iunopn  15194  toponmax  15217  tgtop  15260  tgiun  15265  tgidm  15266  ntropn  15309  tgrest  15361  restopnb  15373  cnovex  15388  cnclima  15415  txvalex  15446  txtop  15452  tx1cn  15461  tx2cn  15462  txcnp  15463  txcnmpt  15465  txdis1cn  15470  cnmptcom  15490  imasnopn  15491  hmeocnv  15499  hmeores  15507  txhmeo  15511  txswaphmeo  15513  ispsmet  15515  xmetres  15574  metres  15575  blex  15579  xmeter  15628  xmetresbl  15632  mopntopon  15635  isxms2  15644  xmetxp  15699  xmettx  15702  txmetcnp  15710  qtopbasss  15713  qtopbas  15714  reopnap  15738  ioo2blex  15744  blssioo  15745  tgioo  15746  fsumcncntop  15759  expcn  15761  cncfval  15764  divccncfap  15782  cdivcncfap  15796  divcncfap  15806  maxcncf  15807  mincncf  15808  ivthdec  15836  hoverb  15840  limccnpcntop  15867  dvrecap  15905  elplyd  15933  ply1termlem  15934  ply1term  15935  plymullem1  15940  plyaddlem  15941  plymullem  15942  plycolemc  15950  plyco  15951  plycj  15953  plycn  15954  plyreres  15956  dvply1  15957  dvply2g  15958  pilem3  15976  tanrpcl  16030  cosordlem  16042  ioocosf1o  16047  logfac  16090  rpcncxpcl  16099  rpcxpcl  16100  rpabscxpbnd  16137  rplogbcl  16143  zprmlogbaplem2  16177  log2tlbndlog2  16181  birthdaylem1g  16186  pellexlem1  16190  efnnfsumcl  16200  ppiqfi  16203  chtqcl  16205  efchtqcl  16207  ppiqcl  16212  sgmnncl  16218  efchtqdvds  16226  prmorcht  16243  mpodvdsmulf1o  16245  fsumdvdsmul  16246  chtublem  16256  mersenne  16258  perfectlem2  16261  bposlem5  16276  bposlem9  16280  lgslem1  16285  lgsval  16289  lgscllem  16292  lgsne0  16323  gausslemma2dlem4  16349  lgseisenlem1  16355  lgsquadlem1  16362  lgsquadlem2  16363  2sqlem3  16402  2sqlem8  16408  vtxex  16425  iedgex  16426  edgvalg  16466  edgopval  16469  edgstruct  16471  usgrausgrien  16576  ausgrumgrien  16577  ausgrusgrien  16578  uspgr1ewopdc  16651  usgr2v1e2w  16653  uhgrspansubgrlem  16683  vtxdgfif  16700  vtxdfifiun  16704  1loopgrvd2fi  16712  1loopgrvd0fi  16713  1hevtxdg0fi  16714  1hevtxdg1en  16715  p1evtxdeqfilem  16718  vdegp1bid  16722  wlkex  16732  wlkelvv  16756  clwwlkccat  16808  clwwlknonex2lem1  16844  clwwlknonex2lem2  16845  clwwlknonex2  16846  trlsegvdeglem6  16872  trlsegvdeglem7  16873  trlsegvdegfi  16874  eupth2lem3lem1fi  16875  eupth2lem3lem2fi  16876  eupth2lem3lem5  16879  eupth2lembfi  16884  eulerpathprum  16887  depindlem1  16913  depindlem2  16914  djucllem  16994  012of  17189  2o01f  17190  nninfsellemeq  17223  qdencn  17238  cvgcmp2nlemabs  17247  trilpolemclim  17252  trilpolemisumle  17254  trilpolemeq1  17256  trilpolemlt1  17257  nconstwlpolemgt0  17281