Theorem eqeltrd 2282

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

Syntax hints:   → wi 4   = wceq 1373   ∈ wcel 2176

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-clel 2201

This theorem is referenced by:  eqeltrrd  2283  3eltr4d  2289  eqeltrid  2292  eqeltrdi  2296  ifcldadc  3600  ifcldcd  3608  intab  3914  disjiun  4039  iinexgm  4198  opexg  4272  tfisi  4635  nnpredcl  4671  imain  5356  fvmptd  5660  fvmptdf  5667  fvmptt  5671  elfvmptrab  5675  dffo3  5727  resfunexg  5805  f1oiso2  5896  riota2df  5920  riota5f  5924  ovmpodxf  6071  ovmpodf  6077  offval  6166  ofvalg  6168  offeq  6172  iunexg  6204  oprabexd  6212  fo1stresm  6247  fo2ndresm  6248  oprssdmm  6257  1stdm  6268  1stconst  6307  2ndconst  6308  cnvf1olem  6310  fo2ndf  6313  f1od2  6321  iunon  6370  tfrlemibacc  6412  tfrlemibfn  6414  tfr1onlembacc  6428  tfr1onlembfn  6430  tfrcllembacc  6441  tfrcllembfn  6443  tfrcl  6450  rdgon  6472  frec0g  6483  freccllem  6488  frecfcllem  6490  frecsuclem  6492  oacl  6546  omcl  6547  oeicl  6548  nntr2  6589  mptelixpg  6821  fidifsnen  6967  en2eqpr  7004  unfiin  7023  tpfidceq  7027  ssfirab  7033  fnfi  7038  relcnvfi  7043  fidcenumlemr  7057  elfi2  7074  supclti  7100  supubti  7101  suplubti  7102  supelti  7104  ordiso2  7137  djulclr  7151  djurclr  7152  djulcl  7153  djurcl  7154  djuss  7172  updjudhcoinlf  7182  updjudhcoinrg  7183  ctssdclemn0  7212  ctssdccl  7213  ctssdc  7215  enumctlemm  7216  nninfwlpoimlemg  7277  cardcl  7288  exmidontriimlem2  7334  exmidapne  7372  cc2lem  7378  cc3  7380  addclpi  7440  mulclpi  7441  addclnq  7488  mulclnq  7489  addclnq0  7564  mulclnq0  7565  nqpnq0nq  7566  elnp1st2nd  7589  prarloclemcalc  7615  distrlem1prl  7695  distrlem1pru  7696  ltexprlemopl  7714  ltexprlemopu  7716  ltexprlemfl  7722  ltexprlemrl  7723  ltexprlemfu  7724  ltexprlemru  7725  addcanprlemu  7728  recexprlemloc  7744  aptiprleml  7752  caucvgprprlemopl  7810  suplocexprlemex  7835  addclsr  7866  mulclsr  7867  recexgt0sr  7886  mulextsr1lem  7893  suplocsrlemb  7919  suplocsrlempr  7920  suplocsrlem  7921  axaddcl  7977  axaddrcl  7978  axmulcl  7979  axmulrcl  7980  axcaucvglemval  8010  subcl  8271  cru  8675  aprcl  8719  aptap  8723  divclap  8751  redivclap  8804  diveqap1bd  8909  lbinfcl  9022  cju  9034  nn1m1nn  9054  nnsub  9075  nnnn0addcl  9325  un0addcl  9328  peano2z  9408  peano2zm  9410  zaddcllemneg  9411  zaddcl  9412  nnaddm1cl  9434  nn0n0n1ge2  9443  zdivadd  9462  zdivmul  9463  suprzclex  9471  zneo  9474  peano5uzti  9481  supinfneg  9716  infsupneg  9717  qmulz  9744  qnegcl  9757  qapne  9760  qdivcl  9764  cnref1o  9772  xnegcl  9954  xltnegi  9957  xaddnemnf  9979  xaddnepnf  9980  xnegdi  9990  xnpcan  9994  xltadd1  9998  xposdif  10004  xleaddadd  10009  iccf1o  10126  ige3m2fz  10171  ige2m1fz1  10231  zssinfcl  10375  infssuzex  10376  infssuzcldc  10378  zsupssdc  10381  suprzcl2dc  10382  rebtwn2z  10397  flqcl  10416  flapcl  10418  ceilqcl  10453  intfracq  10465  modqcl  10471  mulqmod0  10475  modqdifz  10481  zmodcl  10489  modfzo0difsn  10540  modsumfzodifsn  10541  frec2uzzd  10545  frec2uzsucd  10546  frec2uzuzd  10547  frecuzrdgrrn  10553  frec2uzrdg  10554  frecuzrdgrcl  10555  frecuzrdgsuc  10559  frecuzrdgrclt  10560  frecuzrdgg  10561  frecuzrdgsuctlem  10568  fzofig  10577  iseqovex  10603  seq3val  10605  seqvalcd  10606  seqf  10609  seqovcd  10612  seq3clss  10616  seq3caopr3  10636  iseqf1olemnab  10646  iseqf1olemqk  10652  iseqf1olemjpcl  10653  iseqf1olemqpcl  10654  iseqf1olemfvp  10655  seq3f1olemqsumkj  10656  seq3f1olemqsum  10658  seq3f1oleml  10661  seq3f1o  10662  seqf1oglem2a  10663  seqf1oglem1  10664  seqf1oglem2  10665  seq3distr  10677  ser0f  10679  ser3le  10682  exp3vallem  10685  exp3val  10686  exp1  10690  expcl2lemap  10696  m1expcl2  10706  expaddzap  10728  sqcl  10745  nnsqcl  10754  qsqcl  10756  zesq  10803  facp1  10875  faccl  10880  facdiv  10883  bcval  10894  bcrpcl  10898  bcp1n  10906  bcpasc  10911  permnn  10916  hashennn  10925  hashcl  10926  lencl  10998  wrdexg  11005  elovmpowrd  11035  lswcl  11044  ccatcl  11049  ccatrn  11065  lswccatn0lsw  11067  s1cl  11075  swrdclg  11103  swrdwrdsymbg  11117  ccatswrd  11123  shftlem  11127  ovshftex  11130  shftf  11141  seq3shft  11149  cjth  11157  imval  11161  recl  11164  imcl  11165  crre  11168  remim  11171  reim0b  11173  cvg1nlemcau  11295  uzin2  11298  resqrexlem1arp  11316  resqrexlemp1rp  11317  resqrexlemglsq  11333  resqrexlemga  11334  resqrtcl  11340  abscl  11362  absrpclap  11372  nn0abscl  11396  fzomaxdiflem  11423  fzomaxdif  11424  maxabslemab  11517  maxcl  11521  zmaxcl  11535  minmax  11541  mincl  11542  xrmaxcl  11563  xrmaxaddlem  11571  xrminmax  11576  xrmincl  11577  xrmineqinf  11580  xrminrpcl  11585  reccn2ap  11624  climaddc1  11640  climmulc2  11642  climsubc1  11643  climsubc2  11644  climle  11645  climlec2  11652  climcvg1nlem  11660  sumrbdclem  11688  fsum3cvg  11689  summodclem3  11691  summodclem2a  11692  zsumdc  11695  fsumgcl  11697  fsum3  11698  isumss  11702  fisumss  11703  isumss2  11704  fsum3cvg2  11705  fsum3ser  11708  fsumcl2lem  11709  fsumcllem  11710  fsumadd  11717  sumsnf  11720  fsumsplitsn  11721  isumcl  11736  isummulc2  11737  isumrecl  11740  isumge0  11741  isumadd  11742  fsum2dlemstep  11745  fisumcom2  11749  mptfzshft  11753  fsumrev  11754  fsummulc2  11759  iserabs  11786  isumshft  11801  isumsplit  11802  isum1p  11803  isumrpcl  11805  isumle  11806  isumlessdc  11807  trireciplem  11811  expcnvap0  11813  expcnvre  11814  expcnv  11815  explecnv  11816  geolim  11822  geolim2  11823  geo2lim  11827  cvgratnnlemsumlt  11839  cvgratz  11843  mertenslemub  11845  mertenslemi1  11846  mertenslem2  11847  mertensabs  11848  prodf1f  11854  prodfdivap  11858  prodrbdclem  11882  fproddccvg  11883  prodmodclem3  11886  prodmodclem2a  11887  zproddc  11890  fprodseq  11894  fprodntrivap  11895  prodssdc  11900  fprodmul  11902  prodsnf  11903  fprodsplitdc  11907  fprodunsn  11915  fprodcl2lem  11916  fprodcllem  11917  fprodabs  11927  fprodrev  11930  fprod2dlemstep  11933  fprodcom2fi  11937  fprodsplitsn  11944  efcllemp  11969  ef0lem  11971  efcvgfsum  11978  reefcl  11979  ege2le3  11982  efcj  11984  efaddlem  11985  eftlcvg  11998  eftlcl  11999  reeftlcl  12000  eftlub  12001  efsep  12002  effsumlt  12003  efgt1p2  12006  efgt1p  12007  reeff1  12011  tanclap  12020  resincl  12031  recoscl  12032  retanclap  12033  eirraplem  12088  dvdsval2  12101  fsumdvds  12153  sqoddm1div8z  12197  bitsinv1lem  12272  gcdval  12280  gcdn0cl  12283  gcddvds  12284  divgcdnnr  12297  uzwodc  12358  nn0seqcvgd  12363  ialgrlem1st  12364  ialgrlemconst  12365  algrf  12367  algrp1  12368  eucalgf  12377  eucalglt  12379  lcmval  12385  lcmcllem  12389  lcmgcdlem  12399  cncongr2  12426  sqrt2irrlem  12483  oddpwdclemxy  12491  oddpwdclemdc  12495  qden1elz  12527  phicl2  12536  phimullem  12547  eulerthlemth  12554  prmdiv  12557  odzcllem  12565  pythagtriplem8  12595  pythagtriplem9  12596  pcval  12619  pczcl  12621  pcqcl  12629  dvdsprmpweqle  12660  pcaddlem  12662  pcmptcl  12665  pcmpt  12666  pockthlem  12679  pockthg  12680  zgz  12696  gznegcl  12698  gzcjcl  12699  gzaddcl  12700  gzmulcl  12701  gzabssqcl  12704  4sqlem5  12705  4sqlem4a  12714  mul4sqlem  12716  mul4sq  12717  4sqlemafi  12718  4sqlemffi  12719  4sqleminfi  12720  4sqexercise1  12721  4sqlem16  12729  4sqlem17  12730  ennnfonelemjn  12773  ennnfonelemg  12774  ennnfonelemp1  12777  ctinfomlemom  12798  ctiunctlemfo  12810  nninfdclemcl  12819  nninfdclemf  12820  nninfdclemp1  12821  setsex  12864  strsetsid  12865  strslfv3  12878  ressex  12897  ressbas2d  12900  strressid  12903  tgvalex  13095  ptex  13096  prdsex  13101  prdsval  13105  imasex  13137  imasival  13138  imasbas  13139  imasplusg  13140  imasmulr  13141  imasaddfn  13149  imasaddval  13150  imasaddf  13151  imasmulfn  13152  imasmulval  13153  imasmulf  13154  qusval  13155  qusex  13157  qusaddvallemg  13165  qusaddflemg  13166  qusaddval  13167  qusaddf  13168  qusmulval  13169  qusmulf  13170  mgm1  13202  gsumress  13227  gsumprval  13231  prdsplusgsgrpcl  13246  prdsplusgcl  13278  prdsidlem  13279  pwsmnd  13282  mhmex  13294  subsubm  13315  0subm  13316  mhmeql  13324  gsumwsubmcl  13328  gsumfzcl  13331  grpsubval  13378  grplinv  13382  pwsgrp  13443  qusgrp2  13449  mulgval  13458  mulgex  13459  mulgfng  13460  mulg1  13465  mulgnnp1  13466  mulgnnsubcl  13470  mulgnn0subcl  13471  mulgsubcl  13472  mulgnndir  13487  subgex  13512  subgsubcl  13521  issubgrpd  13527  subsubg  13533  nsgconj  13542  0nsg  13550  triv1nsgd  13554  eqgex  13557  eqger  13560  eqgcpbl  13564  ghmex  13591  ghmpreima  13602  ghmnsgpreima  13605  conjnmz  13615  gsumfzsubmcl  13674  mgpex  13687  rngmgpf  13699  qusrng  13720  mgpf  13773  qusring2  13828  opprex  13835  opprrng  13839  opprring  13841  dvdsrex  13860  opprunitd  13872  dvrvald  13896  dvrcl  13897  unitdvcl  13898  invrpropdg  13911  subsubrng  13976  subrgcrng  13987  subrgsubm  13996  subrgugrp  14002  subsubrg  14007  rnrhmsubrg  14014  aprcotr  14047  rmodislmod  14113  lssvsubcl  14128  islss3  14141  lspex  14157  ellspsn  14179  sraex  14208  rlmlmod  14226  lidlex  14235  rspex  14236  lidl0cl  14245  lidlacl  14246  lidlnegcl  14247  ridl0  14272  ridl1  14273  2idlelbas  14278  cnsubglem  14341  expghmap  14369  mulgrhm  14371  zrhex  14383  znbaslemnn  14401  psrval  14428  psrbagfi  14435  psrbasg  14436  mplsubgfilemm  14460  mplsubgfilemcl  14461  mplsubgfileminv  14462  mplgrpfi  14468  iunopn  14474  toponmax  14497  tgtop  14540  tgiun  14545  tgidm  14546  ntropn  14589  tgrest  14641  restopnb  14653  cnovex  14668  cnclima  14695  txvalex  14726  txtop  14732  tx1cn  14741  tx2cn  14742  txcnp  14743  txcnmpt  14745  txdis1cn  14750  cnmptcom  14770  imasnopn  14771  hmeocnv  14779  hmeores  14787  txhmeo  14791  txswaphmeo  14793  ispsmet  14795  xmetres  14854  metres  14855  blex  14859  xmeter  14908  xmetresbl  14912  mopntopon  14915  isxms2  14924  xmetxp  14979  xmettx  14982  txmetcnp  14990  qtopbasss  14993  qtopbas  14994  reopnap  15018  ioo2blex  15024  blssioo  15025  tgioo  15026  fsumcncntop  15039  expcn  15041  cncfval  15044  divccncfap  15062  cdivcncfap  15076  divcncfap  15086  maxcncf  15087  mincncf  15088  ivthdec  15116  hoverb  15120  limccnpcntop  15147  dvrecap  15185  elplyd  15213  ply1termlem  15214  ply1term  15215  plymullem1  15220  plyaddlem  15221  plymullem  15222  plycolemc  15230  plyco  15231  plycj  15233  plycn  15234  plyreres  15236  dvply1  15237  dvply2g  15238  pilem3  15255  tanrpcl  15309  cosordlem  15321  ioocosf1o  15326  rpcncxpcl  15374  rpcxpcl  15375  rpabscxpbnd  15412  rplogbcl  15418  sgmnncl  15460  mpodvdsmulf1o  15462  fsumdvdsmul  15463  mersenne  15469  perfectlem2  15472  lgslem1  15477  lgsval  15481  lgscllem  15484  lgsne0  15515  gausslemma2dlem4  15541  lgseisenlem1  15547  lgsquadlem1  15554  lgsquadlem2  15555  2sqlem3  15594  2sqlem8  15600  edgopval  15654  edgstruct  15656  djucllem  15736  012of  15930  2o01f  15931  nninfsellemeq  15951  qdencn  15966  cvgcmp2nlemabs  15971  trilpolemclim  15975  trilpolemisumle  15977  trilpolemeq1  15979  trilpolemlt1  15980  nconstwlpolemgt0  16003