Theorem eqeltrd 2270

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

Syntax hints:   → wi 4   = wceq 1364   ∈ wcel 2164

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-cleq 2186  df-clel 2189

This theorem is referenced by:  eqeltrrd  2271  3eltr4d  2277  eqeltrid  2280  eqeltrdi  2284  ifcldadc  3586  ifcldcd  3593  intab  3899  disjiun  4024  iinexgm  4183  opexg  4257  tfisi  4619  nnpredcl  4655  imain  5336  fvmptd  5638  fvmptdf  5645  fvmptt  5649  elfvmptrab  5653  dffo3  5705  resfunexg  5779  f1oiso2  5870  riota2df  5894  riota5f  5898  ovmpodxf  6044  ovmpodf  6050  offval  6138  ofvalg  6140  offeq  6144  iunexg  6171  oprabexd  6179  fo1stresm  6214  fo2ndresm  6215  oprssdmm  6224  1stdm  6235  1stconst  6274  2ndconst  6275  cnvf1olem  6277  fo2ndf  6280  f1od2  6288  iunon  6337  tfrlemibacc  6379  tfrlemibfn  6381  tfr1onlembacc  6395  tfr1onlembfn  6397  tfrcllembacc  6408  tfrcllembfn  6410  tfrcl  6417  rdgon  6439  frec0g  6450  freccllem  6455  frecfcllem  6457  frecsuclem  6459  oacl  6513  omcl  6514  oeicl  6515  nntr2  6556  mptelixpg  6788  fidifsnen  6926  en2eqpr  6963  unfiin  6982  ssfirab  6990  fnfi  6995  relcnvfi  7000  fidcenumlemr  7014  elfi2  7031  supclti  7057  supubti  7058  suplubti  7059  supelti  7061  ordiso2  7094  djulclr  7108  djurclr  7109  djulcl  7110  djurcl  7111  djuss  7129  updjudhcoinlf  7139  updjudhcoinrg  7140  ctssdclemn0  7169  ctssdccl  7170  ctssdc  7172  enumctlemm  7173  nninfwlpoimlemg  7234  cardcl  7241  exmidontriimlem2  7282  exmidapne  7320  cc2lem  7326  cc3  7328  addclpi  7387  mulclpi  7388  addclnq  7435  mulclnq  7436  addclnq0  7511  mulclnq0  7512  nqpnq0nq  7513  elnp1st2nd  7536  prarloclemcalc  7562  distrlem1prl  7642  distrlem1pru  7643  ltexprlemopl  7661  ltexprlemopu  7663  ltexprlemfl  7669  ltexprlemrl  7670  ltexprlemfu  7671  ltexprlemru  7672  addcanprlemu  7675  recexprlemloc  7691  aptiprleml  7699  caucvgprprlemopl  7757  suplocexprlemex  7782  addclsr  7813  mulclsr  7814  recexgt0sr  7833  mulextsr1lem  7840  suplocsrlemb  7866  suplocsrlempr  7867  suplocsrlem  7868  axaddcl  7924  axaddrcl  7925  axmulcl  7926  axmulrcl  7927  axcaucvglemval  7957  subcl  8218  cru  8621  aprcl  8665  aptap  8669  divclap  8697  redivclap  8750  diveqap1bd  8855  lbinfcl  8968  cju  8980  nn1m1nn  9000  nnsub  9021  nnnn0addcl  9270  un0addcl  9273  peano2z  9353  peano2zm  9355  zaddcllemneg  9356  zaddcl  9357  nnaddm1cl  9378  nn0n0n1ge2  9387  zdivadd  9406  zdivmul  9407  suprzclex  9415  zneo  9418  peano5uzti  9425  supinfneg  9660  infsupneg  9661  qmulz  9688  qnegcl  9701  qapne  9704  qdivcl  9708  cnref1o  9716  xnegcl  9898  xltnegi  9901  xaddnemnf  9923  xaddnepnf  9924  xnegdi  9934  xnpcan  9938  xltadd1  9942  xposdif  9948  xleaddadd  9953  iccf1o  10070  ige3m2fz  10115  ige2m1fz1  10175  rebtwn2z  10323  flqcl  10342  flapcl  10344  ceilqcl  10379  intfracq  10391  modqcl  10397  mulqmod0  10401  modqdifz  10407  zmodcl  10415  modfzo0difsn  10466  modsumfzodifsn  10467  frec2uzzd  10471  frec2uzsucd  10472  frec2uzuzd  10473  frecuzrdgrrn  10479  frec2uzrdg  10480  frecuzrdgrcl  10481  frecuzrdgsuc  10485  frecuzrdgrclt  10486  frecuzrdgg  10487  frecuzrdgsuctlem  10494  fzofig  10503  iseqovex  10529  seq3val  10531  seqvalcd  10532  seqf  10535  seqovcd  10538  seq3clss  10542  seq3caopr3  10562  iseqf1olemnab  10572  iseqf1olemqk  10578  iseqf1olemjpcl  10579  iseqf1olemqpcl  10580  iseqf1olemfvp  10581  seq3f1olemqsumkj  10582  seq3f1olemqsum  10584  seq3f1oleml  10587  seq3f1o  10588  seqf1oglem2a  10589  seqf1oglem1  10590  seqf1oglem2  10591  seq3distr  10603  ser0f  10605  ser3le  10608  exp3vallem  10611  exp3val  10612  exp1  10616  expcl2lemap  10622  m1expcl2  10632  expaddzap  10654  sqcl  10671  nnsqcl  10680  qsqcl  10682  zesq  10729  facp1  10801  faccl  10806  facdiv  10809  bcval  10820  bcrpcl  10824  bcp1n  10832  bcpasc  10837  permnn  10842  hashennn  10851  hashcl  10852  lencl  10918  wrdexg  10925  elovmpowrd  10955  shftlem  10960  ovshftex  10963  shftf  10974  seq3shft  10982  cjth  10990  imval  10994  recl  10997  imcl  10998  crre  11001  remim  11004  reim0b  11006  cvg1nlemcau  11128  uzin2  11131  resqrexlem1arp  11149  resqrexlemp1rp  11150  resqrexlemglsq  11166  resqrexlemga  11167  resqrtcl  11173  abscl  11195  absrpclap  11205  nn0abscl  11229  fzomaxdiflem  11256  fzomaxdif  11257  maxabslemab  11350  maxcl  11354  zmaxcl  11368  minmax  11373  mincl  11374  xrmaxcl  11395  xrmaxaddlem  11403  xrminmax  11408  xrmincl  11409  xrmineqinf  11412  xrminrpcl  11417  reccn2ap  11456  climaddc1  11472  climmulc2  11474  climsubc1  11475  climsubc2  11476  climle  11477  climlec2  11484  climcvg1nlem  11492  sumrbdclem  11520  fsum3cvg  11521  summodclem3  11523  summodclem2a  11524  zsumdc  11527  fsumgcl  11529  fsum3  11530  isumss  11534  fisumss  11535  isumss2  11536  fsum3cvg2  11537  fsum3ser  11540  fsumcl2lem  11541  fsumcllem  11542  fsumadd  11549  sumsnf  11552  fsumsplitsn  11553  isumcl  11568  isummulc2  11569  isumrecl  11572  isumge0  11573  isumadd  11574  fsum2dlemstep  11577  fisumcom2  11581  mptfzshft  11585  fsumrev  11586  fsummulc2  11591  iserabs  11618  isumshft  11633  isumsplit  11634  isum1p  11635  isumrpcl  11637  isumle  11638  isumlessdc  11639  trireciplem  11643  expcnvap0  11645  expcnvre  11646  expcnv  11647  explecnv  11648  geolim  11654  geolim2  11655  geo2lim  11659  cvgratnnlemsumlt  11671  cvgratz  11675  mertenslemub  11677  mertenslemi1  11678  mertenslem2  11679  mertensabs  11680  prodf1f  11686  prodfdivap  11690  prodrbdclem  11714  fproddccvg  11715  prodmodclem3  11718  prodmodclem2a  11719  zproddc  11722  fprodseq  11726  fprodntrivap  11727  prodssdc  11732  fprodmul  11734  prodsnf  11735  fprodsplitdc  11739  fprodunsn  11747  fprodcl2lem  11748  fprodcllem  11749  fprodabs  11759  fprodrev  11762  fprod2dlemstep  11765  fprodcom2fi  11769  fprodsplitsn  11776  efcllemp  11801  ef0lem  11803  efcvgfsum  11810  reefcl  11811  ege2le3  11814  efcj  11816  efaddlem  11817  eftlcvg  11830  eftlcl  11831  reeftlcl  11832  eftlub  11833  efsep  11834  effsumlt  11835  efgt1p2  11838  efgt1p  11839  reeff1  11843  tanclap  11852  resincl  11863  recoscl  11864  retanclap  11865  eirraplem  11920  dvdsval2  11933  sqoddm1div8z  12027  zssinfcl  12085  infssuzex  12086  infssuzcldc  12088  zsupssdc  12091  suprzcl2dc  12092  gcdval  12096  gcdn0cl  12099  gcddvds  12100  divgcdnnr  12113  uzwodc  12174  nn0seqcvgd  12179  ialgrlem1st  12180  ialgrlemconst  12181  algrf  12183  algrp1  12184  eucalgf  12193  eucalglt  12195  lcmval  12201  lcmcllem  12205  lcmgcdlem  12215  cncongr2  12242  sqrt2irrlem  12299  oddpwdclemxy  12307  oddpwdclemdc  12311  qden1elz  12343  phicl2  12352  phimullem  12363  eulerthlemth  12370  prmdiv  12373  odzcllem  12380  pythagtriplem8  12410  pythagtriplem9  12411  pcval  12434  pczcl  12436  pcqcl  12444  dvdsprmpweqle  12475  pcaddlem  12477  pcmptcl  12480  pcmpt  12481  pockthlem  12494  pockthg  12495  zgz  12511  gznegcl  12513  gzcjcl  12514  gzaddcl  12515  gzmulcl  12516  gzabssqcl  12519  4sqlem5  12520  4sqlem4a  12529  mul4sqlem  12531  mul4sq  12532  4sqlemafi  12533  4sqlemffi  12534  4sqleminfi  12535  4sqexercise1  12536  4sqlem16  12544  4sqlem17  12545  ennnfonelemjn  12559  ennnfonelemg  12560  ennnfonelemp1  12563  ctinfomlemom  12584  ctiunctlemfo  12596  nninfdclemcl  12605  nninfdclemf  12606  nninfdclemp1  12607  setsex  12650  strsetsid  12651  ressex  12683  ressbas2d  12686  strressid  12689  tgvalex  12874  ptex  12875  prdsex  12880  imasex  12888  imasival  12889  imasbas  12890  imasplusg  12891  imasmulr  12892  imasaddfn  12900  imasaddval  12901  imasaddf  12902  imasmulfn  12903  imasmulval  12904  imasmulf  12905  qusval  12906  qusex  12908  qusaddvallemg  12916  qusaddflemg  12917  qusaddval  12918  qusaddf  12919  qusmulval  12920  qusmulf  12921  mgm1  12953  gsumress  12978  gsumprval  12982  mhmex  13034  subsubm  13055  0subm  13056  mhmeql  13064  gsumwsubmcl  13068  gsumfzcl  13071  grpsubval  13118  grplinv  13122  qusgrp2  13183  mulgval  13192  mulgex  13193  mulgfng  13194  mulg1  13199  mulgnnp1  13200  mulgnnsubcl  13204  mulgnn0subcl  13205  mulgsubcl  13206  mulgnndir  13221  subgex  13246  subgsubcl  13255  issubgrpd  13261  subsubg  13267  nsgconj  13276  0nsg  13284  triv1nsgd  13288  eqgex  13291  eqger  13294  eqgcpbl  13298  ghmex  13325  ghmpreima  13336  ghmnsgpreima  13339  conjnmz  13349  gsumfzsubmcl  13408  mgpex  13421  rngmgpf  13433  qusrng  13454  mgpf  13507  qusring2  13562  opprex  13569  opprrng  13573  opprring  13575  dvdsrex  13594  opprunitd  13606  dvrvald  13630  dvrcl  13631  unitdvcl  13632  invrpropdg  13645  subsubrng  13710  subrgcrng  13721  subrgsubm  13730  subrgugrp  13736  subsubrg  13741  rnrhmsubrg  13748  aprcotr  13781  rmodislmod  13847  lssvsubcl  13862  islss3  13875  lspex  13891  ellspsn  13913  sraex  13942  rlmlmod  13960  lidlex  13969  rspex  13970  lidl0cl  13979  lidlacl  13980  lidlnegcl  13981  ridl0  14006  ridl1  14007  2idlelbas  14012  cnsubglem  14067  expghmap  14095  mulgrhm  14097  zrhex  14109  znbaslemnn  14127  psrval  14152  psrbasg  14159  iunopn  14170  toponmax  14193  tgtop  14236  tgiun  14241  tgidm  14242  ntropn  14285  tgrest  14337  restopnb  14349  cnovex  14364  cnclima  14391  txvalex  14422  txtop  14428  tx1cn  14437  tx2cn  14438  txcnp  14439  txcnmpt  14441  txdis1cn  14446  cnmptcom  14466  imasnopn  14467  hmeocnv  14475  hmeores  14483  txhmeo  14487  txswaphmeo  14489  ispsmet  14491  xmetres  14550  metres  14551  blex  14555  xmeter  14604  xmetresbl  14608  mopntopon  14611  isxms2  14620  xmetxp  14675  xmettx  14678  txmetcnp  14686  qtopbasss  14689  qtopbas  14690  reopnap  14706  ioo2blex  14712  blssioo  14713  tgioo  14714  fsumcncntop  14724  cncfval  14727  divccncfap  14745  cdivcncfap  14758  divcncfap  14768  maxcncf  14769  mincncf  14770  ivthdec  14798  hoverb  14802  limccnpcntop  14829  dvrecap  14862  elplyd  14887  ply1termlem  14888  ply1term  14889  plymullem1  14894  plyaddlem  14895  plymullem  14896  pilem3  14918  tanrpcl  14972  cosordlem  14984  ioocosf1o  14989  rpcncxpcl  15037  rpcxpcl  15038  rpabscxpbnd  15073  rplogbcl  15078  lgslem1  15116  lgsval  15120  lgscllem  15123  lgsne0  15154  gausslemma2dlem4  15180  lgseisenlem1  15186  lgsquadlem1  15191  2sqlem3  15204  2sqlem8  15210  djucllem  15292  012of  15486  2o01f  15487  nninfsellemeq  15504  qdencn  15517  cvgcmp2nlemabs  15522  trilpolemclim  15526  trilpolemisumle  15528  trilpolemeq1  15530  trilpolemlt1  15531  nconstwlpolemgt0  15554