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  4292  opexg  4370  tfisi  4736  nnpredcl  4772  opabssxpd  4813  imain  5466  fvmptd  5789  fvmptdf  5796  fvmptt  5800  elfvmptrab  5805  dffo3  5858  resfunexg  5939  f1oiso2  6036  riota2df  6063  riota5f  6068  ovmpodxf  6217  ovmpodf  6223  ofovex  6311  offval  6314  ofvalg  6316  offeq  6320  iunexg  6352  oprabexd  6364  fo1stresm  6399  fo2ndresm  6400  oprssdmm  6409  1stdm  6420  1stconst  6461  2ndconst  6462  cnvf1olem  6464  fo2ndf  6467  f1od2  6475  iunon  6559  tfrlemibacc  6601  tfrlemibfn  6603  tfr1onlembacc  6617  tfr1onlembfn  6619  tfrcllembacc  6630  tfrcllembfn  6632  tfrcl  6639  rdgon  6661  frec0g  6672  freccllem  6677  frecfcllem  6679  frecsuclem  6681  oacl  6737  omcl  6738  oeicl  6739  nntr2  6780  mptelixpg  7020  fidifsnen  7176  en2eqpr  7218  unfiin  7237  tpfidceq  7241  ssfirab  7248  fnfi  7254  relcnvfi  7259  fidcenumlemr  7277  snopfsuppdc  7304  fsuppcorn  7306  elfi2  7311  supclti  7344  supubti  7345  suplubti  7346  supelti  7348  ordiso2  7381  djulclr  7395  djurclr  7396  djulcl  7397  djurcl  7398  djuss  7416  updjudhcoinlf  7426  updjudhcoinrg  7427  ctssdclemn0  7456  ctssdccl  7457  ctssdc  7459  enumctlemm  7460  nninfwlpoimlemg  7521  cardcl  7532  exmidontriimlem2  7584  exmidapne  7632  cc2lem  7638  cc3  7640  addclpi  7700  mulclpi  7701  addclnq  7748  mulclnq  7749  addclnq0  7824  mulclnq0  7825  nqpnq0nq  7826  elnp1st2nd  7849  prarloclemcalc  7875  distrlem1prl  7955  distrlem1pru  7956  ltexprlemopl  7974  ltexprlemopu  7976  ltexprlemfl  7982  ltexprlemrl  7983  ltexprlemfu  7984  ltexprlemru  7985  addcanprlemu  7988  recexprlemloc  8004  aptiprleml  8012  caucvgprprlemopl  8070  suplocexprlemex  8095  addclsr  8126  mulclsr  8127  recexgt0sr  8146  mulextsr1lem  8153  suplocsrlemb  8179  suplocsrlempr  8180  suplocsrlem  8181  axaddcl  8237  axaddrcl  8238  axmulcl  8239  axmulrcl  8240  axcaucvglemval  8270  subcl  8532  cru  8938  aprcl  8982  aptap  8986  divclap  9016  redivclap  9069  diveqap1bd  9174  lbinfcl  9287  cju  9299  nn1m1nn  9331  nnsub  9352  nnnn0addcl  9604  un0addcl  9607  peano2z  9691  peano2zm  9693  zaddcllemneg  9694  zaddcl  9695  nnaddm1cl  9717  nn0n0n1ge2  9726  zdivadd  9746  zdivmul  9747  suprzclex  9755  zneo  9758  peano5uzti  9765  supinfneg  10011  infsupneg  10012  qmulz  10039  qnegcl  10052  qapne  10055  qdivcl  10059  cnref1o  10068  xnegcl  10251  xltnegi  10254  xaddnemnf  10276  xaddnepnf  10277  xnegdi  10287  xnpcan  10291  xltadd1  10295  xposdif  10301  xleaddadd  10306  iccf1o  10424  ige3m2fz  10471  ige2m1fz1  10533  zssinfcl  10682  infssuzex  10683  infssuzcldc  10685  zsupssdc  10690  suprzcl2dc  10691  rebtwn2z  10706  flqcl  10725  flapclz  10727  ceilqcl  10766  intfracq  10778  modqcl  10784  mulqmod0  10788  modqdifz  10794  zmodcl  10802  modfzo0difsn  10853  modsumfzodifsn  10854  frec2uzzd  10858  frec2uzsucd  10859  frec2uzuzd  10860  frecuzrdgrrn  10866  frec2uzrdg  10867  frecuzrdgrcl  10868  frecuzrdgsuc  10872  frecuzrdgrclt  10873  frecuzrdgg  10874  frecuzrdgsuctlem  10881  fzofig  10890  iseqovex  10916  seq3val  10918  seqvalcd  10919  seqf  10922  seqovcd  10925  seq3clss  10929  seq3caopr3  10949  iseqf1olemnab  10959  iseqf1olemqk  10965  iseqf1olemjpcl  10966  iseqf1olemqpcl  10967  iseqf1olemfvp  10968  seq3f1olemqsumkj  10969  seq3f1olemqsum  10971  seq3f1oleml  10974  seq3f1o  10975  seqf1oglem2a  10976  seqf1oglem1  10977  seqf1oglem2  10978  seq3distr  10990  ser0f  10992  ser3le  10995  exp3vallem  10998  exp3val  10999  exp1  11003  expcl2lemap  11009  m1expcl2  11019  expaddzap  11041  sqcl  11058  nnsqcl  11067  qsqcl  11069  zesq  11117  facp1  11190  faccl  11195  facdiv  11198  bcval  11209  bcrpcl  11213  bcp1n  11221  bcpasc  11226  permnn  11232  hashennn  11241  hashcl  11242  hashf1  11309  lencl  11330  wrdexg  11337  elovmpowrd  11368  lswcl  11377  ccatcl  11383  ccatrn  11399  lswccatn0lsw  11401  ccatalpha  11403  s1cl  11411  swrdclg  11444  swrdwrdsymbg  11458  ccatswrd  11464  pfxval  11468  fnpfx  11471  pfxclg  11472  pfxwrdsymbg  11484  ccatpfx  11495  lenrevpfxcctswrd  11506  wrdind  11516  wrd2ind  11517  shftlem  11603  ovshftex  11606  shftf  11617  seq3shft  11625  cjth  11633  imval  11637  recl  11640  imcl  11641  crre  11644  remim  11647  reim0b  11649  cvg1nlemcau  11772  uzin2  11775  resqrexlem1arp  11793  resqrexlemp1rp  11794  resqrexlemglsq  11810  resqrexlemga  11811  resqrtcl  11817  abscl  11839  absrpclap  11849  qabscl  11865  nn0abscl  11874  fzomaxdiflem  11901  fzomaxdif  11902  maxabslemab  11995  maxcl  11999  zmaxcl  12013  minmax  12020  mincl  12021  zmincl  12029  xrmaxcl  12043  xrmaxaddlem  12051  xrminmax  12056  xrmincl  12057  xrmineqinf  12060  xrminrpcl  12065  reccn2ap  12104  climaddc1  12120  climmulc2  12122  climsubc1  12123  climsubc2  12124  climle  12125  climlec2  12132  climcvg1nlem  12140  sumrbdclem  12169  fsum3cvg  12170  summodclem3  12172  summodclem2a  12173  zsumdc  12176  fsumgcl  12178  fsum3  12179  isumss  12183  fisumss  12184  isumss2  12185  fsum3cvg2  12186  fsum3ser  12189  fsumcl2lem  12190  fsumcllem  12191  fsumadd  12198  sumsnf  12201  fsumsplitsn  12202  isumcl  12217  isummulc2  12218  isumrecl  12221  isumge0  12222  isumadd  12223  fsum2dlemstep  12226  fisumcom2  12230  mptfzshft  12234  fsumrev  12235  fsummulc2  12240  iserabs  12267  isumshft  12282  isumsplit  12283  isum1p  12284  isumrpcl  12286  isumle  12287  isumlessdc  12288  trireciplem  12292  expcnvap0  12294  expcnvre  12295  expcnv  12296  explecnv  12297  geolim  12303  geolim2  12304  geo2lim  12308  cvgratnnlemsumlt  12320  cvgratz  12324  mertenslemub  12326  mertenslemi1  12327  mertenslem2  12328  mertensabs  12329  prodf1f  12335  prodfdivap  12339  prodrbdclem  12363  fproddccvg  12364  prodmodclem3  12367  prodmodclem2a  12368  zproddc  12371  fprodseq  12375  fprodntrivap  12376  prodssdc  12381  fprodmul  12383  prodsnf  12384  fprodsplitdc  12388  fprodunsn  12396  fprodcl2lem  12397  fprodcllem  12398  fprodabs  12408  fprodrev  12411  fprod2dlemstep  12414  fprodcom2fi  12418  fprodsplitsn  12425  efcllemp  12450  ef0lem  12452  efcvgfsum  12459  reefcl  12460  ege2le3  12463  efcj  12465  efaddlem  12466  eftlcvg  12479  eftlcl  12480  reeftlcl  12481  eftlub  12482  efsep  12483  effsumlt  12484  efgt1p2  12487  efgt1p  12488  reeff1  12492  tanclap  12501  resincl  12512  recoscl  12513  retanclap  12514  eirraplem  12569  dvdsval2  12582  fsumdvds  12634  sqoddm1div8z  12678  bitsinv1lem  12753  gcdval  12761  gcdn0cl  12764  gcddvds  12765  divgcdnnr  12778  uzwodc  12839  nn0seqcvgd  12844  ialgrlem1st  12845  ialgrlemconst  12846  algrf  12848  algrp1  12849  eucalgf  12858  eucalglt  12860  lcmval  12866  lcmcllem  12870  lcmgcdlem  12880  cncongr2  12907  sqrt2irrlem  12965  nnmaxpwlemxy  12973  nnmaxpwlemparts  12977  qden1elz  13010  nn0sqdcq  13013  sqrtrirr  13014  phicl2  13021  phimullem  13032  eulerthlemth  13039  prmdiv  13042  odzcllem  13050  pythagtriplem8  13080  pythagtriplem9  13081  pcval  13104  pczcl  13106  pcqcl  13114  dvdsprmpweqle  13145  pcaddlem  13147  pcmptcl  13150  pcmpt  13151  pockthlem  13164  pockthg  13165  zgz  13181  gznegcl  13183  gzcjcl  13184  gzaddcl  13185  gzmulcl  13186  gzabssqcl  13189  4sqlem5  13190  4sqlem4a  13199  mul4sqlem  13201  mul4sq  13202  4sqlemafi  13203  4sqlemffi  13204  4sqleminfi  13205  4sqexercise1  13206  4sqlem16  13214  4sqlem17  13215  ballotfilemfelz  13288  ballotfilemiex  13302  ballotfilemsdom  13313  ballotfilemgval  13325  ennnfonelemjn  13351  ennnfonelemg  13352  ennnfonelemp1  13355  ctinfomlemom  13376  ctiunctlemfo  13388  nninfdclemcl  13397  nninfdclemf  13398  nninfdclemp1  13399  setsex  13442  strsetsid  13443  strslfv3  13456  bassetsnn  13467  ressex  13477  ressbas2d  13481  strressid  13484  tgvalex  13676  ptex  13677  imasex  13685  imasival  13686  imasbas  13687  imasplusg  13688  imasmulr  13689  imasaddfn  13697  imasaddval  13698  imasaddf  13699  imasmulfn  13700  imasmulval  13701  imasmulf  13702  qusval  13703  qusex  13705  qusaddvallemg  13713  qusaddflemg  13714  qusaddval  13715  qusaddf  13716  qusmulval  13717  qusmulf  13718  mgm1  13749  gzsumress  13771  mhmex  13828  subsubm  13849  0subm  13850  mhmeql  13858  gzsumwsubmcl  13860  gzsumcl  13863  grpsubval  13910  grplinv  13914  qusgrp2  13975  mulgval  13984  mulgex  13985  mulgfng  13986  mulg1  13991  mulgnnp1  13992  mulgnnsubcl  13996  mulgnn0subcl  13997  mulgsubcl  13998  mulgnndir  14013  subgex  14038  subgsubcl  14047  issubgrpd  14053  subsubg  14059  nsgconj  14068  0nsg  14076  triv1nsgd  14080  eqgex  14083  eqger  14086  eqgcpbl  14090  ghmex  14117  ghmpreima  14128  ghmnsgpreima  14131  conjnmz  14141  cntzex  14150  cntrsubgnsg  14175  gzsumsubmcl  14232  gzsumsplit0  14238  gsumvalfi  14242  gsumsncmn  14246  gsumclfi  14249  gsumsubmclfi  14253  gsumsnfdcmn  14257  gsumunsnfd  14259  gsum2dfi  14273  gsum2d2fi  14274  prdsex  14279  prdsval  14280  prdsplusgsgrpcl  14297  prdsplusgcl  14299  prdsidlem  14300  pwsmnd  14319  pwsgrp  14321  mgpex  14330  rngmgpf  14343  qusrng  14364  mgpf  14422  qusring2  14480  opprex  14487  opprrng  14491  opprring  14493  dvdsrex  14514  opprunitd  14526  dvrvald  14550  dvrcl  14551  unitdvcl  14552  invrpropdg  14565  subsubrng  14631  subrgcrng  14642  subrgsubm  14651  subrgugrp  14657  subsubrg  14662  rnrhmsubrg  14669  aprcotr  14706  aprnzr  14708  aprlring  14709  rmodislmod  14797  lssvsubcl  14812  islss3  14825  lspex  14841  ellspsn  14863  sraex  14892  rlmlmod  14910  lidlex  14919  rspex  14920  lidl0cl  14929  lidlacl  14930  lidlnegcl  14931  ridl0  14956  ridl1  14957  2idlelbas  14962  cnsubglem  15025  expghmap  15051  mulgrhm  15053  zrhex  15065  znbaslemnn  15083  asplss  15125  aspsubrg  15127  psrval  15159  psrbagfi  15168  psrbagcon  15171  psrbasg  15178  psrlidmfi  15199  psrridmfi  15200  mplsubgfilemm  15214  mplsubgfilemcl  15215  mplsubgfileminv  15216  mplgrpfi  15222  iunopn  15228  toponmax  15251  tgtop  15294  tgiun  15299  tgidm  15300  ntropn  15343  tgrest  15395  restopnb  15407  cnovex  15422  cnclima  15449  txvalex  15480  txtop  15486  tx1cn  15495  tx2cn  15496  txcnp  15497  txcnmpt  15499  txdis1cn  15504  cnmptcom  15524  imasnopn  15525  hmeocnv  15533  hmeores  15541  txhmeo  15545  txswaphmeo  15547  ispsmet  15549  xmetres  15608  metres  15609  blex  15613  xmeter  15662  xmetresbl  15666  mopntopon  15669  isxms2  15678  xmetxp  15733  xmettx  15736  txmetcnp  15744  qtopbasss  15747  qtopbas  15748  reopnap  15772  ioo2blex  15778  blssioo  15779  tgioo  15780  fsumcncntop  15793  expcn  15795  cncfval  15798  divccncfap  15816  cdivcncfap  15830  divcncfap  15840  maxcncf  15841  mincncf  15842  ivthdec  15870  hoverb  15874  limccnpcntop  15901  dvrecap  15939  elplyd  15967  ply1termlem  15968  ply1term  15969  plymullem1  15974  plyaddlem  15975  plymullem  15976  plycolemc  15984  plyco  15985  plycj  15987  plycn  15988  plyreres  15990  dvply1  15991  dvply2g  15992  pilem3  16010  tanrpcl  16064  cosordlem  16077  ioocosf1o  16082  logfac  16126  rpcncxpcl  16135  rpcxpcl  16136  rpabscxpbnd  16175  rplogbcl  16182  zprmlogbaplem2  16216  log2tlbndlog2  16220  birthdaylem1g  16225  pellexlem1  16229  efnnfsumcl  16239  ppiqfi  16242  chtqcl  16244  efchtqcl  16246  ppiqcl  16251  sgmnncl  16257  efchtqdvds  16265  prmorcht  16282  mpodvdsmulf1o  16284  fsumdvdsmul  16285  chtublem  16295  mersenne  16297  perfectlem2  16300  bposlem5  16315  bposlem9  16319  lgslem1  16324  lgsval  16328  lgscllem  16331  lgsne0  16362  gausslemma2dlem4  16388  lgseisenlem1  16394  lgsquadlem1  16401  lgsquadlem2  16402  2sqlem3  16441  2sqlem8  16447  vtxex  16464  iedgex  16465  edgvalg  16505  edgopval  16508  edgstruct  16510  usgrausgrien  16615  ausgrumgrien  16616  ausgrusgrien  16617  uspgr1ewopdc  16690  usgr2v1e2w  16692  uhgrspansubgrlem  16722  vtxdgfif  16739  vtxdfifiun  16743  1loopgrvd2fi  16751  1loopgrvd0fi  16752  1hevtxdg0fi  16753  1hevtxdg1en  16754  p1evtxdeqfilem  16757  vdegp1bid  16761  wlkex  16771  wlkelvv  16795  clwwlkccat  16847  clwwlknonex2lem1  16883  clwwlknonex2lem2  16884  clwwlknonex2  16885  trlsegvdeglem6  16911  trlsegvdeglem7  16912  trlsegvdegfi  16913  eupth2lem3lem1fi  16914  eupth2lem3lem2fi  16915  eupth2lem3lem5  16918  eupth2lembfi  16923  eulerpathprum  16926  depindlem1  16952  depindlem2  16953  djucllem  17033  012of  17228  2o01f  17229  idjudju  17252  nninfsellemeq  17263  qdencn  17278  cvgcmp2nlemabs  17287  trilpolemclim  17292  trilpolemisumle  17294  trilpolemeq1  17296  trilpolemlt1  17297  nconstwlpolemgt0  17321