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  6560  tfrlemibacc  6602  tfrlemibfn  6604  tfr1onlembacc  6618  tfr1onlembfn  6620  tfrcllembacc  6631  tfrcllembfn  6633  tfrcl  6640  rdgon  6662  frec0g  6673  freccllem  6678  frecfcllem  6680  frecsuclem  6682  oacl  6738  omcl  6739  oeicl  6740  nntr2  6781  mptelixpg  7022  fidifsnen  7178  en2eqpr  7220  unfiin  7239  tpfidceq  7243  ssfirab  7250  fnfi  7256  relcnvfi  7261  fidcenumlemr  7279  fdmfifsupp  7301  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  9689  peano2zm  9691  zaddcllemneg  9692  zaddcl  9693  nnaddm1cl  9715  nn0n0n1ge2  9724  zdivadd  9745  zdivmul  9746  suprzclex  9754  zneo  9757  peano5uzti  9764  supinfneg  10010  infsupneg  10011  qmulz  10038  qnegcl  10051  qapne  10054  qdivcl  10058  cnref1o  10067  xnegcl  10250  xltnegi  10253  xaddnemnf  10275  xaddnepnf  10276  xnegdi  10286  xnpcan  10290  xltadd1  10294  xposdif  10300  xleaddadd  10305  iccf1o  10423  ige3m2fz  10470  ige2m1fz1  10532  zssinfcl  10681  infssuzex  10682  infssuzcldc  10684  zsupssdc  10689  suprzcl2dc  10690  rebtwn2z  10705  flqcl  10724  flapclz  10726  ceilqcl  10765  intfracq  10777  modqcl  10783  mulqmod0  10787  modqdifz  10793  zmodcl  10801  modfzo0difsn  10852  modsumfzodifsn  10853  frec2uzzd  10857  frec2uzsucd  10858  frec2uzuzd  10859  frecuzrdgrrn  10865  frec2uzrdg  10866  frecuzrdgrcl  10867  frecuzrdgsuc  10871  frecuzrdgrclt  10872  frecuzrdgg  10873  frecuzrdgsuctlem  10880  fzofig  10889  iseqovex  10915  seq3val  10917  seqvalcd  10918  seqf  10921  seqovcd  10924  seq3clss  10928  seq3caopr3  10948  iseqf1olemnab  10958  iseqf1olemqk  10964  iseqf1olemjpcl  10965  iseqf1olemqpcl  10966  iseqf1olemfvp  10967  seq3f1olemqsumkj  10968  seq3f1olemqsum  10970  seq3f1oleml  10973  seq3f1o  10974  seqf1oglem2a  10975  seqf1oglem1  10976  seqf1oglem2  10977  seq3distr  10989  ser0f  10991  ser3le  10994  exp3vallem  10997  exp3val  10998  exp1  11002  expcl2lemap  11008  m1expcl2  11018  expaddzap  11040  sqcl  11057  nnsqcl  11066  qsqcl  11068  zesq  11116  facp1  11189  faccl  11194  facdiv  11197  bcval  11208  bcrpcl  11212  bcp1n  11220  bcpasc  11225  permnn  11231  hashennn  11240  hashcl  11241  hashf1  11308  lencl  11329  wrdexg  11336  elovmpowrd  11367  lswcl  11376  ccatcl  11382  ccatrn  11398  lswccatn0lsw  11400  ccatalpha  11402  s1cl  11410  swrdclg  11443  swrdwrdsymbg  11457  ccatswrd  11463  pfxval  11467  fnpfx  11470  pfxclg  11471  pfxwrdsymbg  11483  ccatpfx  11494  lenrevpfxcctswrd  11505  wrdind  11515  wrd2ind  11516  shftlem  11602  ovshftex  11605  shftf  11616  seq3shft  11624  cjth  11632  imval  11636  recl  11639  imcl  11640  crre  11643  remim  11646  reim0b  11648  cvg1nlemcau  11771  uzin2  11774  resqrexlem1arp  11792  resqrexlemp1rp  11793  resqrexlemglsq  11809  resqrexlemga  11810  resqrtcl  11816  abscl  11838  absrpclap  11848  qabscl  11864  nn0abscl  11873  fzomaxdiflem  11900  fzomaxdif  11901  maxabslemab  11994  maxcl  11998  zmaxcl  12012  minmax  12019  mincl  12020  zmincl  12028  xrmaxcl  12042  xrmaxaddlem  12050  xrminmax  12055  xrmincl  12056  xrmineqinf  12059  xrminrpcl  12064  reccn2ap  12103  climaddc1  12119  climmulc2  12121  climsubc1  12122  climsubc2  12123  climle  12124  climlec2  12131  climcvg1nlem  12139  sumrbdclem  12168  fsum3cvg  12169  summodclem3  12171  summodclem2a  12172  zsumdc  12175  fsumgcl  12177  fsum3  12178  isumss  12182  fisumss  12183  isumss2  12184  fsum3cvg2  12185  fsum3ser  12188  fsumcl2lem  12189  fsumcllem  12190  fsumadd  12197  sumsnf  12200  fsumsplitsn  12201  isumcl  12216  isummulc2  12217  isumrecl  12220  isumge0  12221  isumadd  12222  fsum2dlemstep  12225  fisumcom2  12229  mptfzshft  12233  fsumrev  12234  fsummulc2  12239  iserabs  12266  isumshft  12281  isumsplit  12282  isum1p  12283  isumrpcl  12285  isumle  12286  isumlessdc  12287  trireciplem  12291  expcnvap0  12293  expcnvre  12294  expcnv  12295  explecnv  12296  geolim  12302  geolim2  12303  geo2lim  12307  cvgratnnlemsumlt  12319  cvgratz  12323  mertenslemub  12325  mertenslemi1  12326  mertenslem2  12327  mertensabs  12328  prodf1f  12334  prodfdivap  12338  prodrbdclem  12362  fproddccvg  12363  prodmodclem3  12366  prodmodclem2a  12367  zproddc  12370  fprodseq  12374  fprodntrivap  12375  prodssdc  12380  fprodmul  12382  prodsnf  12383  fprodsplitdc  12387  fprodunsn  12395  fprodcl2lem  12396  fprodcllem  12397  fprodabs  12407  fprodrev  12410  fprod2dlemstep  12413  fprodcom2fi  12417  fprodsplitsn  12424  efcllemp  12449  ef0lem  12451  efcvgfsum  12458  reefcl  12459  ege2le3  12462  efcj  12464  efaddlem  12465  eftlcvg  12478  eftlcl  12479  reeftlcl  12480  eftlub  12481  efsep  12482  effsumlt  12483  efgt1p2  12486  efgt1p  12487  reeff1  12491  tanclap  12500  resincl  12511  recoscl  12512  retanclap  12513  eirraplem  12568  dvdsval2  12581  fsumdvds  12633  sqoddm1div8z  12677  bitsinv1lem  12752  gcdval  12760  gcdn0cl  12763  gcddvds  12764  divgcdnnr  12777  uzwodc  12838  nn0seqcvgd  12843  ialgrlem1st  12844  ialgrlemconst  12845  algrf  12847  algrp1  12848  eucalgf  12857  eucalglt  12859  lcmval  12865  lcmcllem  12869  lcmgcdlem  12879  cncongr2  12906  sqrt2irrlem  12964  nnmaxpwlemxy  12972  nnmaxpwlemparts  12976  qden1elz  13009  nn0sqdcq  13012  sqrtrirr  13013  phicl2  13020  phimullem  13031  eulerthlemth  13038  prmdiv  13041  odzcllem  13049  pythagtriplem8  13079  pythagtriplem9  13080  pcval  13103  pczcl  13105  pcqcl  13113  dvdsprmpweqle  13144  pcaddlem  13146  pcmptcl  13149  pcmpt  13150  pockthlem  13163  pockthg  13164  zgz  13180  gznegcl  13182  gzcjcl  13183  gzaddcl  13184  gzmulcl  13185  gzabssqcl  13188  4sqlem5  13189  4sqlem4a  13198  mul4sqlem  13200  mul4sq  13201  4sqlemafi  13202  4sqlemffi  13203  4sqleminfi  13204  4sqexercise1  13205  4sqlem16  13213  4sqlem17  13214  ballotfilemfelz  13287  ballotfilemiex  13301  ballotfilemsdom  13312  ballotfilemgval  13324  ennnfonelemjn  13350  ennnfonelemg  13351  ennnfonelemp1  13354  ctinfomlemom  13375  ctiunctlemfo  13387  nninfdclemcl  13396  nninfdclemf  13397  nninfdclemp1  13398  setsex  13441  strsetsid  13442  strslfv3  13455  bassetsnn  13466  ressex  13476  ressbas2d  13480  strressid  13483  tgvalex  13675  ptex  13676  imasex  13684  imasival  13685  imasbas  13686  imasplusg  13687  imasmulr  13688  imasaddfn  13696  imasaddval  13697  imasaddf  13698  imasmulfn  13699  imasmulval  13700  imasmulf  13701  qusval  13702  qusex  13704  qusaddvallemg  13712  qusaddflemg  13713  qusaddval  13714  qusaddf  13715  qusmulval  13716  qusmulf  13717  mgm1  13748  gzsumress  13770  mhmex  13827  subsubm  13848  0subm  13849  mhmeql  13857  gzsumwsubmcl  13859  gzsumcl  13862  grpsubval  13909  grplinv  13913  qusgrp2  13974  mulgval  13983  mulgex  13984  mulgfng  13985  mulg1  13990  mulgnnp1  13991  mulgnnsubcl  13995  mulgnn0subcl  13996  mulgsubcl  13997  mulgnndir  14012  subgex  14037  subgsubcl  14046  issubgrpd  14052  subsubg  14058  nsgconj  14067  0nsg  14075  triv1nsgd  14079  eqgex  14082  eqger  14085  eqgcpbl  14089  ghmex  14116  ghmpreima  14127  ghmnsgpreima  14130  conjnmz  14140  cntzex  14149  cntrsubgnsg  14174  gzsumsubmcl  14231  gzsumsplit0  14237  gsumvalfi  14241  gsumsncmn  14245  gsumclfi  14248  gsumsubmclfi  14252  gsumsnfdcmn  14256  gsumunsnfd  14258  gsum2dfi  14272  gsum2d2fi  14273  prdsex  14278  prdsval  14279  prdsplusgsgrpcl  14296  prdsplusgcl  14298  prdsidlem  14299  pwsmnd  14318  pwsgrp  14320  mgpex  14329  rngmgpf  14342  qusrng  14363  mgpf  14421  qusring2  14479  opprex  14486  opprrng  14490  opprring  14492  dvdsrex  14513  opprunitd  14525  dvrvald  14549  dvrcl  14550  unitdvcl  14551  invrpropdg  14564  subsubrng  14630  subrgcrng  14641  subrgsubm  14650  subrgugrp  14656  subsubrg  14661  rnrhmsubrg  14668  aprcotr  14705  aprnzr  14707  aprlring  14708  rmodislmod  14796  lssvsubcl  14811  islss3  14824  lspex  14840  ellspsn  14862  sraex  14891  rlmlmod  14909  lidlex  14918  rspex  14919  lidl0cl  14928  lidlacl  14929  lidlnegcl  14930  ridl0  14955  ridl1  14956  2idlelbas  14961  cnsubglem  15024  expghmap  15050  mulgrhm  15052  zrhex  15064  znbaslemnn  15082  asplss  15124  aspsubrg  15126  psrval  15160  psrbagfi  15166  psrbagcon  15174  psrbasg  15187  psrlidmfi  15208  psrridmfi  15209  mvrval2  15216  mplsubgfilemm  15231  mplsubgfilemcl  15232  mplsubgfileminv  15233  mplgrpfi  15239  iunopn  15245  toponmax  15268  tgtop  15311  tgiun  15316  tgidm  15317  ntropn  15360  tgrest  15412  restopnb  15424  cnovex  15439  cnclima  15466  txvalex  15497  txtop  15503  tx1cn  15512  tx2cn  15513  txcnp  15514  txcnmpt  15516  txdis1cn  15521  cnmptcom  15541  imasnopn  15542  hmeocnv  15550  hmeores  15558  txhmeo  15562  txswaphmeo  15564  ispsmet  15566  xmetres  15625  metres  15626  blex  15630  xmeter  15679  xmetresbl  15683  mopntopon  15686  isxms2  15695  xmetxp  15750  xmettx  15753  txmetcnp  15761  qtopbasss  15764  qtopbas  15765  reopnap  15789  ioo2blex  15795  blssioo  15796  tgioo  15797  fsumcncntop  15810  expcn  15812  cncfval  15815  divccncfap  15833  cdivcncfap  15847  divcncfap  15857  maxcncf  15858  mincncf  15859  ivthdec  15887  hoverb  15891  limccnpcntop  15918  dvrecap  15956  elplyd  15984  ply1termlem  15985  ply1term  15986  plymullem1  15991  plyaddlem  15992  plymullem  15993  plycolemc  16001  plyco  16002  plycj  16004  plycn  16005  plyreres  16007  dvply1  16008  dvply2g  16009  pilem3  16027  tanrpcl  16081  cosordlem  16094  ioocosf1o  16099  logfac  16143  rpcncxpcl  16152  rpcxpcl  16153  rpabscxpbnd  16192  rplogbcl  16199  zprmlogbaplem2  16233  log2tlbndlog2  16237  birthdaylem1g  16242  pellexlem1  16246  efnnfsumcl  16256  ppiqfi  16259  chtqcl  16261  efchtqcl  16263  ppiqcl  16268  sgmnncl  16274  efchtqdvds  16282  prmorcht  16299  mpodvdsmulf1o  16301  fsumdvdsmul  16302  chtublem  16312  mersenne  16314  perfectlem2  16317  bposlem5  16332  bposlem9  16336  lgslem1  16341  lgsval  16345  lgscllem  16348  lgsne0  16379  gausslemma2dlem4  16405  lgseisenlem1  16411  lgsquadlem1  16418  lgsquadlem2  16419  2sqlem3  16458  2sqlem8  16464  vtxex  16481  iedgex  16482  edgvalg  16522  edgopval  16525  edgstruct  16527  usgrausgrien  16632  ausgrumgrien  16633  ausgrusgrien  16634  uspgr1ewopdc  16707  usgr2v1e2w  16709  uhgrspansubgrlem  16739  vtxdgfif  16756  vtxdfifiun  16760  1loopgrvd2fi  16768  1loopgrvd0fi  16769  1hevtxdg0fi  16770  1hevtxdg1en  16771  p1evtxdeqfilem  16774  vdegp1bid  16778  wlkex  16788  wlkelvv  16812  clwwlkccat  16864  clwwlknonex2lem1  16900  clwwlknonex2lem2  16901  clwwlknonex2  16902  trlsegvdeglem6  16928  trlsegvdeglem7  16929  trlsegvdegfi  16930  eupth2lem3lem1fi  16931  eupth2lem3lem2fi  16932  eupth2lem3lem5  16935  eupth2lembfi  16940  eulerpathprum  16943  depindlem1  16969  depindlem2  16970  djucllem  17050  012of  17245  2o01f  17246  idjudju  17269  nninfsellemeq  17280  qdencn  17295  cvgcmp2nlemabs  17304  trilpolemclim  17309  trilpolemisumle  17311  trilpolemeq1  17313  trilpolemlt1  17314  nconstwlpolemgt0  17338