Theorem eqeltrd 2254

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

Syntax hints:   → wi 4   = wceq 1353   ∈ wcel 2148

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173

This theorem is referenced by:  eqeltrrd  2255  3eltr4d  2261  eqeltrid  2264  eqeltrdi  2268  ifcldadc  3565  ifcldcd  3572  intab  3875  disjiun  4000  iinexgm  4156  opexg  4230  tfisi  4588  nnpredcl  4624  imain  5300  fvmptd  5600  fvmptdf  5606  fvmptt  5610  elfvmptrab  5614  dffo3  5666  resfunexg  5740  f1oiso2  5831  riota2df  5854  riota5f  5858  ovmpodxf  6003  ovmpodf  6009  offval  6093  ofvalg  6095  offeq  6099  iunexg  6123  oprabexd  6131  fo1stresm  6165  fo2ndresm  6166  oprssdmm  6175  1stdm  6186  1stconst  6225  2ndconst  6226  cnvf1olem  6228  fo2ndf  6231  f1od2  6239  iunon  6288  tfrlemibacc  6330  tfrlemibfn  6332  tfr1onlembacc  6346  tfr1onlembfn  6348  tfrcllembacc  6359  tfrcllembfn  6361  tfrcl  6368  rdgon  6390  frec0g  6401  freccllem  6406  frecfcllem  6408  frecsuclem  6410  oacl  6464  omcl  6465  oeicl  6466  nntr2  6507  mptelixpg  6737  fidifsnen  6873  en2eqpr  6910  unfiin  6928  ssfirab  6936  fnfi  6939  relcnvfi  6943  fidcenumlemr  6957  elfi2  6974  supclti  7000  supubti  7001  suplubti  7002  supelti  7004  ordiso2  7037  djulclr  7051  djurclr  7052  djulcl  7053  djurcl  7054  djuss  7072  updjudhcoinlf  7082  updjudhcoinrg  7083  ctssdclemn0  7112  ctssdccl  7113  ctssdc  7115  enumctlemm  7116  nninfwlpoimlemg  7176  cardcl  7183  exmidontriimlem2  7224  exmidapne  7262  cc2lem  7268  cc3  7270  addclpi  7329  mulclpi  7330  addclnq  7377  mulclnq  7378  addclnq0  7453  mulclnq0  7454  nqpnq0nq  7455  elnp1st2nd  7478  prarloclemcalc  7504  distrlem1prl  7584  distrlem1pru  7585  ltexprlemopl  7603  ltexprlemopu  7605  ltexprlemfl  7611  ltexprlemrl  7612  ltexprlemfu  7613  ltexprlemru  7614  addcanprlemu  7617  recexprlemloc  7633  aptiprleml  7641  caucvgprprlemopl  7699  suplocexprlemex  7724  addclsr  7755  mulclsr  7756  recexgt0sr  7775  mulextsr1lem  7782  suplocsrlemb  7808  suplocsrlempr  7809  suplocsrlem  7810  axaddcl  7866  axaddrcl  7867  axmulcl  7868  axmulrcl  7869  axcaucvglemval  7899  subcl  8159  cru  8562  aprcl  8606  aptap  8610  divclap  8638  redivclap  8691  diveqap1bd  8796  lbinfcl  8909  cju  8921  nn1m1nn  8940  nnsub  8961  nnnn0addcl  9209  un0addcl  9212  peano2z  9292  peano2zm  9294  zaddcllemneg  9295  zaddcl  9296  nnaddm1cl  9317  nn0n0n1ge2  9326  zdivadd  9345  zdivmul  9346  suprzclex  9354  zneo  9357  peano5uzti  9364  supinfneg  9598  infsupneg  9599  qmulz  9626  qnegcl  9639  qapne  9642  qdivcl  9646  cnref1o  9653  xnegcl  9835  xltnegi  9838  xaddnemnf  9860  xaddnepnf  9861  xnegdi  9871  xnpcan  9875  xltadd1  9879  xposdif  9885  xleaddadd  9890  iccf1o  10007  ige3m2fz  10052  ige2m1fz1  10112  rebtwn2z  10258  flqcl  10276  flapcl  10278  ceilqcl  10311  intfracq  10323  modqcl  10329  mulqmod0  10333  modqdifz  10339  zmodcl  10347  modfzo0difsn  10398  modsumfzodifsn  10399  frec2uzzd  10403  frec2uzsucd  10404  frec2uzuzd  10405  frecuzrdgrrn  10411  frec2uzrdg  10412  frecuzrdgrcl  10413  frecuzrdgsuc  10417  frecuzrdgrclt  10418  frecuzrdgg  10419  frecuzrdgsuctlem  10426  fzofig  10435  iseqovex  10459  seq3val  10461  seqvalcd  10462  seqf  10464  seqovcd  10466  seq3clss  10470  seq3caopr3  10484  iseqf1olemnab  10491  iseqf1olemqk  10497  iseqf1olemjpcl  10498  iseqf1olemqpcl  10499  iseqf1olemfvp  10500  seq3f1olemqsumkj  10501  seq3f1olemqsum  10503  seq3f1oleml  10506  seq3f1o  10507  seq3distr  10516  ser0f  10518  ser3le  10521  exp3vallem  10524  exp3val  10525  exp1  10529  expcl2lemap  10535  m1expcl2  10545  expaddzap  10567  sqcl  10584  nnsqcl  10593  qsqcl  10595  zesq  10642  facp1  10713  faccl  10718  facdiv  10721  bcval  10732  bcrpcl  10736  bcp1n  10744  bcpasc  10749  permnn  10754  hashennn  10763  hashcl  10764  shftlem  10828  ovshftex  10831  shftf  10842  seq3shft  10850  cjth  10858  imval  10862  recl  10865  imcl  10866  crre  10869  remim  10872  reim0b  10874  cvg1nlemcau  10996  uzin2  10999  resqrexlem1arp  11017  resqrexlemp1rp  11018  resqrexlemglsq  11034  resqrexlemga  11035  resqrtcl  11041  abscl  11063  absrpclap  11073  nn0abscl  11097  fzomaxdiflem  11124  fzomaxdif  11125  maxabslemab  11218  maxcl  11222  zmaxcl  11236  minmax  11241  mincl  11242  xrmaxcl  11263  xrmaxaddlem  11271  xrminmax  11276  xrmincl  11277  xrmineqinf  11280  xrminrpcl  11285  reccn2ap  11324  climaddc1  11340  climmulc2  11342  climsubc1  11343  climsubc2  11344  climle  11345  climlec2  11352  climcvg1nlem  11360  sumrbdclem  11388  fsum3cvg  11389  summodclem3  11391  summodclem2a  11392  zsumdc  11395  fsumgcl  11397  fsum3  11398  isumss  11402  fisumss  11403  isumss2  11404  fsum3cvg2  11405  fsum3ser  11408  fsumcl2lem  11409  fsumcllem  11410  fsumadd  11417  sumsnf  11420  fsumsplitsn  11421  isumcl  11436  isummulc2  11437  isumrecl  11440  isumge0  11441  isumadd  11442  fsum2dlemstep  11445  fisumcom2  11449  mptfzshft  11453  fsumrev  11454  fsummulc2  11459  iserabs  11486  isumshft  11501  isumsplit  11502  isum1p  11503  isumrpcl  11505  isumle  11506  isumlessdc  11507  trireciplem  11511  expcnvap0  11513  expcnvre  11514  expcnv  11515  explecnv  11516  geolim  11522  geolim2  11523  geo2lim  11527  cvgratnnlemsumlt  11539  cvgratz  11543  mertenslemub  11545  mertenslemi1  11546  mertenslem2  11547  mertensabs  11548  prodf1f  11554  prodfdivap  11558  prodrbdclem  11582  fproddccvg  11583  prodmodclem3  11586  prodmodclem2a  11587  zproddc  11590  fprodseq  11594  fprodntrivap  11595  prodssdc  11600  fprodmul  11602  prodsnf  11603  fprodsplitdc  11607  fprodunsn  11615  fprodcl2lem  11616  fprodcllem  11617  fprodabs  11627  fprodrev  11630  fprod2dlemstep  11633  fprodcom2fi  11637  fprodsplitsn  11644  efcllemp  11669  ef0lem  11671  efcvgfsum  11678  reefcl  11679  ege2le3  11682  efcj  11684  efaddlem  11685  eftlcvg  11698  eftlcl  11699  reeftlcl  11700  eftlub  11701  efsep  11702  effsumlt  11703  efgt1p2  11706  efgt1p  11707  reeff1  11711  tanclap  11720  resincl  11731  recoscl  11732  retanclap  11733  eirraplem  11787  dvdsval2  11800  sqoddm1div8z  11894  zssinfcl  11952  infssuzex  11953  infssuzcldc  11955  zsupssdc  11958  suprzcl2dc  11959  gcdval  11963  gcdn0cl  11966  gcddvds  11967  divgcdnnr  11980  uzwodc  12041  nn0seqcvgd  12044  ialgrlem1st  12045  ialgrlemconst  12046  algrf  12048  algrp1  12049  eucalgf  12058  eucalglt  12060  lcmval  12066  lcmcllem  12070  lcmgcdlem  12080  cncongr2  12107  sqrt2irrlem  12164  oddpwdclemxy  12172  oddpwdclemdc  12176  qden1elz  12208  phicl2  12217  phimullem  12228  eulerthlemth  12235  prmdiv  12238  odzcllem  12245  pythagtriplem8  12275  pythagtriplem9  12276  pcval  12299  pczcl  12301  pcqcl  12309  dvdsprmpweqle  12339  pcaddlem  12341  pcmptcl  12343  pcmpt  12344  pockthlem  12357  pockthg  12358  zgz  12374  gznegcl  12376  gzcjcl  12377  gzaddcl  12378  gzmulcl  12379  gzabssqcl  12382  4sqlem5  12383  4sqlem4a  12392  mul4sqlem  12394  mul4sq  12395  ennnfonelemjn  12406  ennnfonelemg  12407  ennnfonelemp1  12410  ctinfomlemom  12431  ctiunctlemfo  12443  nninfdclemcl  12452  nninfdclemf  12453  nninfdclemp1  12454  setsex  12497  strsetsid  12498  ressex  12528  ressbas2d  12531  strressid  12533  tgvalex  12718  ptex  12719  prdsex  12724  imasex  12732  imasival  12733  imasbas  12734  imasplusg  12735  imasmulr  12736  imasaddfn  12744  imasaddval  12745  imasaddf  12746  imasmulfn  12747  imasmulval  12748  imasmulf  12749  qusval  12750  qusaddvallemg  12758  qusaddflemg  12759  qusaddval  12760  qusaddf  12761  qusmulval  12762  qusmulf  12763  mgm1  12795  0subm  12877  mhmeql  12882  grpsubval  12925  grplinv  12928  mulgval  12992  mulgfng  12993  mulg1  12996  mulgnnp1  12997  mulgnnsubcl  13001  mulgnn0subcl  13002  mulgsubcl  13003  mulgnndir  13018  subgex  13042  subgsubcl  13051  issubgrpd  13057  subsubg  13063  nsgconj  13072  0nsg  13080  triv1nsgd  13084  eqger  13089  eqgcpbl  13093  mgpex  13141  mgpf  13200  opprex  13251  opprring  13255  dvdsrex  13273  opprunitd  13285  dvrvald  13309  dvrcl  13310  unitdvcl  13311  invrpropdg  13324  subrgcrng  13352  subrgsubm  13361  subrgugrp  13367  subsubrg  13372  aprcotr  13381  rmodislmod  13447  lssvsubcl  13459  islss3  13472  lspsnel  13509  sraex  13538  rlmlmod  13555  lidl0cl  13568  lidlacl  13569  lidlnegcl  13570  cnsubglem  13613  iunopn  13642  toponmax  13665  tgtop  13708  tgiun  13713  tgidm  13714  ntropn  13757  tgrest  13809  restopnb  13821  cnovex  13836  cnclima  13863  txvalex  13894  txtop  13900  tx1cn  13909  tx2cn  13910  txcnp  13911  txcnmpt  13913  txdis1cn  13918  cnmptcom  13938  imasnopn  13939  hmeocnv  13947  hmeores  13955  txhmeo  13959  txswaphmeo  13961  ispsmet  13963  xmetres  14022  metres  14023  blex  14027  xmeter  14076  xmetresbl  14080  mopntopon  14083  isxms2  14092  xmetxp  14147  xmettx  14150  txmetcnp  14158  qtopbasss  14161  qtopbas  14162  reopnap  14178  ioo2blex  14184  blssioo  14185  tgioo  14186  fsumcncntop  14196  cncfval  14199  divccncfap  14217  cdivcncfap  14227  ivthdec  14262  limccnpcntop  14284  dvrecap  14317  pilem3  14344  tanrpcl  14398  cosordlem  14410  ioocosf1o  14415  rpcncxpcl  14463  rpcxpcl  14464  rpabscxpbnd  14499  rplogbcl  14504  lgslem1  14541  lgsval  14545  lgscllem  14548  lgsne0  14579  lgseisenlem1  14590  2sqlem3  14604  2sqlem8  14610  djucllem  14692  012of  14886  2o01f  14887  nninfsellemeq  14904  qdencn  14916  cvgcmp2nlemabs  14921  trilpolemclim  14925  trilpolemisumle  14927  trilpolemeq1  14929  trilpolemlt1  14930  nconstwlpolemgt0  14953