Theorem eqeltrd 2309

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 2301	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))
4	1, 3	mpbird 167	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1398   ∈ wcel 2203

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-cleq 2225  df-clel 2228

This theorem is referenced by:  eqeltrrd  2310  3eltr4d  2316  eqeltrid  2319  eqeltrdi  2323  ifcldadc  3652  ifcldcd  3660  intab  3978  disjiun  4104  iinexgm  4266  opexg  4344  tfisi  4709  nnpredcl  4745  opabssxpd  4786  imain  5438  fvmptd  5758  fvmptdf  5765  fvmptt  5769  elfvmptrab  5773  dffo3  5824  resfunexg  5905  f1oiso2  6000  riota2df  6025  riota5f  6030  ovmpodxf  6179  ovmpodf  6185  offval  6274  ofvalg  6276  offeq  6280  iunexg  6312  oprabexd  6320  fo1stresm  6355  fo2ndresm  6356  oprssdmm  6365  1stdm  6376  1stconst  6417  2ndconst  6418  cnvf1olem  6420  fo2ndf  6423  f1od2  6431  iunon  6515  tfrlemibacc  6557  tfrlemibfn  6559  tfr1onlembacc  6573  tfr1onlembfn  6575  tfrcllembacc  6586  tfrcllembfn  6588  tfrcl  6595  rdgon  6617  frec0g  6628  freccllem  6633  frecfcllem  6635  frecsuclem  6637  oacl  6693  omcl  6694  oeicl  6695  nntr2  6736  mptelixpg  6969  fidifsnen  7125  en2eqpr  7167  unfiin  7186  tpfidceq  7190  ssfirab  7197  fnfi  7203  relcnvfi  7208  fidcenumlemr  7225  snopfsuppdc  7252  fsuppcorn  7254  elfi2  7259  supclti  7289  supubti  7290  suplubti  7291  supelti  7293  ordiso2  7326  djulclr  7340  djurclr  7341  djulcl  7342  djurcl  7343  djuss  7361  updjudhcoinlf  7371  updjudhcoinrg  7372  ctssdclemn0  7401  ctssdccl  7402  ctssdc  7404  enumctlemm  7405  nninfwlpoimlemg  7466  cardcl  7477  exmidontriimlem2  7529  exmidapne  7574  cc2lem  7580  cc3  7582  addclpi  7642  mulclpi  7643  addclnq  7690  mulclnq  7691  addclnq0  7766  mulclnq0  7767  nqpnq0nq  7768  elnp1st2nd  7791  prarloclemcalc  7817  distrlem1prl  7897  distrlem1pru  7898  ltexprlemopl  7916  ltexprlemopu  7918  ltexprlemfl  7924  ltexprlemrl  7925  ltexprlemfu  7926  ltexprlemru  7927  addcanprlemu  7930  recexprlemloc  7946  aptiprleml  7954  caucvgprprlemopl  8012  suplocexprlemex  8037  addclsr  8068  mulclsr  8069  recexgt0sr  8088  mulextsr1lem  8095  suplocsrlemb  8121  suplocsrlempr  8122  suplocsrlem  8123  axaddcl  8179  axaddrcl  8180  axmulcl  8181  axmulrcl  8182  axcaucvglemval  8212  subcl  8472  cru  8876  aprcl  8920  aptap  8924  divclap  8952  redivclap  9005  diveqap1bd  9110  lbinfcl  9223  cju  9235  nn1m1nn  9255  nnsub  9276  nnnn0addcl  9526  un0addcl  9529  peano2z  9613  peano2zm  9615  zaddcllemneg  9616  zaddcl  9617  nnaddm1cl  9639  nn0n0n1ge2  9648  zdivadd  9667  zdivmul  9668  suprzclex  9676  zneo  9679  peano5uzti  9686  supinfneg  9927  infsupneg  9928  qmulz  9955  qnegcl  9968  qapne  9971  qdivcl  9975  cnref1o  9983  xnegcl  10165  xltnegi  10168  xaddnemnf  10190  xaddnepnf  10191  xnegdi  10201  xnpcan  10205  xltadd1  10209  xposdif  10215  xleaddadd  10220  iccf1o  10338  ige3m2fz  10383  ige2m1fz1  10443  zssinfcl  10592  infssuzex  10593  infssuzcldc  10595  zsupssdc  10598  suprzcl2dc  10599  rebtwn2z  10614  flqcl  10633  flapcl  10635  ceilqcl  10670  intfracq  10682  modqcl  10688  mulqmod0  10692  modqdifz  10698  zmodcl  10706  modfzo0difsn  10757  modsumfzodifsn  10758  frec2uzzd  10762  frec2uzsucd  10763  frec2uzuzd  10764  frecuzrdgrrn  10770  frec2uzrdg  10771  frecuzrdgrcl  10772  frecuzrdgsuc  10776  frecuzrdgrclt  10777  frecuzrdgg  10778  frecuzrdgsuctlem  10785  fzofig  10794  iseqovex  10820  seq3val  10822  seqvalcd  10823  seqf  10826  seqovcd  10829  seq3clss  10833  seq3caopr3  10853  iseqf1olemnab  10863  iseqf1olemqk  10869  iseqf1olemjpcl  10870  iseqf1olemqpcl  10871  iseqf1olemfvp  10872  seq3f1olemqsumkj  10873  seq3f1olemqsum  10875  seq3f1oleml  10878  seq3f1o  10879  seqf1oglem2a  10880  seqf1oglem1  10881  seqf1oglem2  10882  seq3distr  10894  ser0f  10896  ser3le  10899  exp3vallem  10902  exp3val  10903  exp1  10907  expcl2lemap  10913  m1expcl2  10923  expaddzap  10945  sqcl  10962  nnsqcl  10971  qsqcl  10973  zesq  11020  facp1  11092  faccl  11097  facdiv  11100  bcval  11111  bcrpcl  11115  bcp1n  11123  bcpasc  11128  permnn  11134  hashennn  11143  hashcl  11144  lencl  11228  wrdexg  11235  elovmpowrd  11266  lswcl  11275  ccatcl  11281  ccatrn  11297  lswccatn0lsw  11299  ccatalpha  11301  s1cl  11309  swrdclg  11342  swrdwrdsymbg  11356  ccatswrd  11362  pfxval  11366  fnpfx  11369  pfxclg  11370  pfxwrdsymbg  11382  ccatpfx  11393  lenrevpfxcctswrd  11404  wrdind  11414  wrd2ind  11415  shftlem  11501  ovshftex  11504  shftf  11515  seq3shft  11523  cjth  11531  imval  11535  recl  11538  imcl  11539  crre  11542  remim  11545  reim0b  11547  cvg1nlemcau  11669  uzin2  11672  resqrexlem1arp  11690  resqrexlemp1rp  11691  resqrexlemglsq  11707  resqrexlemga  11708  resqrtcl  11714  abscl  11736  absrpclap  11746  nn0abscl  11770  fzomaxdiflem  11797  fzomaxdif  11798  maxabslemab  11891  maxcl  11895  zmaxcl  11909  minmax  11915  mincl  11916  xrmaxcl  11937  xrmaxaddlem  11945  xrminmax  11950  xrmincl  11951  xrmineqinf  11954  xrminrpcl  11959  reccn2ap  11998  climaddc1  12014  climmulc2  12016  climsubc1  12017  climsubc2  12018  climle  12019  climlec2  12026  climcvg1nlem  12034  sumrbdclem  12063  fsum3cvg  12064  summodclem3  12066  summodclem2a  12067  zsumdc  12070  fsumgcl  12072  fsum3  12073  isumss  12077  fisumss  12078  isumss2  12079  fsum3cvg2  12080  fsum3ser  12083  fsumcl2lem  12084  fsumcllem  12085  fsumadd  12092  sumsnf  12095  fsumsplitsn  12096  isumcl  12111  isummulc2  12112  isumrecl  12115  isumge0  12116  isumadd  12117  fsum2dlemstep  12120  fisumcom2  12124  mptfzshft  12128  fsumrev  12129  fsummulc2  12134  iserabs  12161  isumshft  12176  isumsplit  12177  isum1p  12178  isumrpcl  12180  isumle  12181  isumlessdc  12182  trireciplem  12186  expcnvap0  12188  expcnvre  12189  expcnv  12190  explecnv  12191  geolim  12197  geolim2  12198  geo2lim  12202  cvgratnnlemsumlt  12214  cvgratz  12218  mertenslemub  12220  mertenslemi1  12221  mertenslem2  12222  mertensabs  12223  prodf1f  12229  prodfdivap  12233  prodrbdclem  12257  fproddccvg  12258  prodmodclem3  12261  prodmodclem2a  12262  zproddc  12265  fprodseq  12269  fprodntrivap  12270  prodssdc  12275  fprodmul  12277  prodsnf  12278  fprodsplitdc  12282  fprodunsn  12290  fprodcl2lem  12291  fprodcllem  12292  fprodabs  12302  fprodrev  12305  fprod2dlemstep  12308  fprodcom2fi  12312  fprodsplitsn  12319  efcllemp  12344  ef0lem  12346  efcvgfsum  12353  reefcl  12354  ege2le3  12357  efcj  12359  efaddlem  12360  eftlcvg  12373  eftlcl  12374  reeftlcl  12375  eftlub  12376  efsep  12377  effsumlt  12378  efgt1p2  12381  efgt1p  12382  reeff1  12386  tanclap  12395  resincl  12406  recoscl  12407  retanclap  12408  eirraplem  12463  dvdsval2  12476  fsumdvds  12528  sqoddm1div8z  12572  bitsinv1lem  12647  gcdval  12655  gcdn0cl  12658  gcddvds  12659  divgcdnnr  12672  uzwodc  12733  nn0seqcvgd  12738  ialgrlem1st  12739  ialgrlemconst  12740  algrf  12742  algrp1  12743  eucalgf  12752  eucalglt  12754  lcmval  12760  lcmcllem  12764  lcmgcdlem  12774  cncongr2  12801  sqrt2irrlem  12858  oddpwdclemxy  12866  oddpwdclemdc  12870  qden1elz  12902  phicl2  12911  phimullem  12922  eulerthlemth  12929  prmdiv  12932  odzcllem  12940  pythagtriplem8  12970  pythagtriplem9  12971  pcval  12994  pczcl  12996  pcqcl  13004  dvdsprmpweqle  13035  pcaddlem  13037  pcmptcl  13040  pcmpt  13041  pockthlem  13054  pockthg  13055  zgz  13071  gznegcl  13073  gzcjcl  13074  gzaddcl  13075  gzmulcl  13076  gzabssqcl  13079  4sqlem5  13080  4sqlem4a  13089  mul4sqlem  13091  mul4sq  13092  4sqlemafi  13093  4sqlemffi  13094  4sqleminfi  13095  4sqexercise1  13096  4sqlem16  13104  4sqlem17  13105  ennnfonelemjn  13153  ennnfonelemg  13154  ennnfonelemp1  13157  ctinfomlemom  13178  ctiunctlemfo  13190  nninfdclemcl  13199  nninfdclemf  13200  nninfdclemp1  13201  setsex  13244  strsetsid  13245  strslfv3  13258  bassetsnn  13269  ressex  13278  ressbas2d  13281  strressid  13284  tgvalex  13476  ptex  13477  prdsex  13482  prdsval  13486  imasex  13518  imasival  13519  imasbas  13520  imasplusg  13521  imasmulr  13522  imasaddfn  13530  imasaddval  13531  imasaddf  13532  imasmulfn  13533  imasmulval  13534  imasmulf  13535  qusval  13536  qusex  13538  qusaddvallemg  13546  qusaddflemg  13547  qusaddval  13548  qusaddf  13549  qusmulval  13550  qusmulf  13551  mgm1  13583  gsumress  13608  gsumprval  13612  prdsplusgsgrpcl  13627  prdsplusgcl  13659  prdsidlem  13660  pwsmnd  13663  mhmex  13675  subsubm  13696  0subm  13697  mhmeql  13705  gsumwsubmcl  13709  gsumfzcl  13712  grpsubval  13759  grplinv  13763  pwsgrp  13824  qusgrp2  13830  mulgval  13839  mulgex  13840  mulgfng  13841  mulg1  13846  mulgnnp1  13847  mulgnnsubcl  13851  mulgnn0subcl  13852  mulgsubcl  13853  mulgnndir  13868  subgex  13893  subgsubcl  13902  issubgrpd  13908  subsubg  13914  nsgconj  13923  0nsg  13931  triv1nsgd  13935  eqgex  13938  eqger  13941  eqgcpbl  13945  ghmex  13972  ghmpreima  13983  ghmnsgpreima  13986  conjnmz  13996  gsumfzsubmcl  14055  gsumsplit0  14063  mgpex  14069  rngmgpf  14081  qusrng  14102  mgpf  14155  qusring2  14210  opprex  14217  opprrng  14221  opprring  14223  dvdsrex  14243  opprunitd  14255  dvrvald  14279  dvrcl  14280  unitdvcl  14281  invrpropdg  14294  subsubrng  14359  subrgcrng  14370  subrgsubm  14379  subrgugrp  14385  subsubrg  14390  rnrhmsubrg  14397  aprcotr  14431  aprnzr  14433  aprlring  14434  rmodislmod  14499  lssvsubcl  14514  islss3  14527  lspex  14543  ellspsn  14565  sraex  14594  rlmlmod  14612  lidlex  14621  rspex  14622  lidl0cl  14631  lidlacl  14632  lidlnegcl  14633  ridl0  14658  ridl1  14659  2idlelbas  14664  cnsubglem  14727  expghmap  14755  mulgrhm  14757  zrhex  14769  znbaslemnn  14787  psrval  14814  psrbagfi  14823  psrbagcon  14826  psrbasg  14829  mplsubgfilemm  14853  mplsubgfilemcl  14854  mplsubgfileminv  14855  mplgrpfi  14861  iunopn  14867  toponmax  14890  tgtop  14933  tgiun  14938  tgidm  14939  ntropn  14982  tgrest  15034  restopnb  15046  cnovex  15061  cnclima  15088  txvalex  15119  txtop  15125  tx1cn  15134  tx2cn  15135  txcnp  15136  txcnmpt  15138  txdis1cn  15143  cnmptcom  15163  imasnopn  15164  hmeocnv  15172  hmeores  15180  txhmeo  15184  txswaphmeo  15186  ispsmet  15188  xmetres  15247  metres  15248  blex  15252  xmeter  15301  xmetresbl  15305  mopntopon  15308  isxms2  15317  xmetxp  15372  xmettx  15375  txmetcnp  15383  qtopbasss  15386  qtopbas  15387  reopnap  15411  ioo2blex  15417  blssioo  15418  tgioo  15419  fsumcncntop  15432  expcn  15434  cncfval  15437  divccncfap  15455  cdivcncfap  15469  divcncfap  15479  maxcncf  15480  mincncf  15481  ivthdec  15509  hoverb  15513  limccnpcntop  15540  dvrecap  15578  elplyd  15606  ply1termlem  15607  ply1term  15608  plymullem1  15613  plyaddlem  15614  plymullem  15615  plycolemc  15623  plyco  15624  plycj  15626  plycn  15627  plyreres  15629  dvply1  15630  dvply2g  15631  pilem3  15648  tanrpcl  15702  cosordlem  15714  ioocosf1o  15719  rpcncxpcl  15767  rpcxpcl  15768  rpabscxpbnd  15805  rplogbcl  15811  pellexlem1  15845  sgmnncl  15856  mpodvdsmulf1o  15858  fsumdvdsmul  15859  mersenne  15865  perfectlem2  15868  lgslem1  15873  lgsval  15877  lgscllem  15880  lgsne0  15911  gausslemma2dlem4  15937  lgseisenlem1  15943  lgsquadlem1  15950  lgsquadlem2  15951  2sqlem3  15990  2sqlem8  15996  vtxex  16013  iedgex  16014  edgvalg  16054  edgopval  16057  edgstruct  16059  usgrausgrien  16164  ausgrumgrien  16165  ausgrusgrien  16166  uspgr1ewopdc  16239  usgr2v1e2w  16241  uhgrspansubgrlem  16271  vtxdgfif  16288  vtxdfifiun  16292  1loopgrvd2fi  16300  1loopgrvd0fi  16301  1hevtxdg0fi  16302  1hevtxdg1en  16303  p1evtxdeqfilem  16306  vdegp1bid  16310  wlkex  16320  wlkelvv  16344  clwwlkccat  16396  clwwlknonex2lem1  16432  clwwlknonex2lem2  16433  clwwlknonex2  16434  trlsegvdeglem6  16460  trlsegvdeglem7  16461  trlsegvdegfi  16462  eupth2lem3lem1fi  16463  eupth2lem3lem2fi  16464  eupth2lem3lem5  16467  eupth2lembfi  16472  eulerpathprum  16475  depindlem1  16501  depindlem2  16502  djucllem  16572  012of  16767  2o01f  16768  nninfsellemeq  16792  qdencn  16807  cvgcmp2nlemabs  16816  trilpolemclim  16820  trilpolemisumle  16822  trilpolemeq1  16824  trilpolemlt1  16825  nconstwlpolemgt0  16850  gfsumval  16862  gfsumsn  16867  gfsumcl  16870