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  5599  fvmptdf  5605  fvmptt  5609  elfvmptrab  5613  dffo3  5665  resfunexg  5739  f1oiso2  5830  riota2df  5853  riota5f  5857  ovmpodxf  6002  ovmpodf  6008  offval  6092  ofvalg  6094  offeq  6098  iunexg  6122  oprabexd  6130  fo1stresm  6164  fo2ndresm  6165  oprssdmm  6174  1stdm  6185  1stconst  6224  2ndconst  6225  cnvf1olem  6227  fo2ndf  6230  f1od2  6238  iunon  6287  tfrlemibacc  6329  tfrlemibfn  6331  tfr1onlembacc  6345  tfr1onlembfn  6347  tfrcllembacc  6358  tfrcllembfn  6360  tfrcl  6367  rdgon  6389  frec0g  6400  freccllem  6405  frecfcllem  6407  frecsuclem  6409  oacl  6463  omcl  6464  oeicl  6465  nntr2  6506  mptelixpg  6736  fidifsnen  6872  en2eqpr  6909  unfiin  6927  ssfirab  6935  fnfi  6938  relcnvfi  6942  fidcenumlemr  6956  elfi2  6973  supclti  6999  supubti  7000  suplubti  7001  supelti  7003  ordiso2  7036  djulclr  7050  djurclr  7051  djulcl  7052  djurcl  7053  djuss  7071  updjudhcoinlf  7081  updjudhcoinrg  7082  ctssdclemn0  7111  ctssdccl  7112  ctssdc  7114  enumctlemm  7115  nninfwlpoimlemg  7175  cardcl  7182  exmidontriimlem2  7223  exmidapne  7261  cc2lem  7267  cc3  7269  addclpi  7328  mulclpi  7329  addclnq  7376  mulclnq  7377  addclnq0  7452  mulclnq0  7453  nqpnq0nq  7454  elnp1st2nd  7477  prarloclemcalc  7503  distrlem1prl  7583  distrlem1pru  7584  ltexprlemopl  7602  ltexprlemopu  7604  ltexprlemfl  7610  ltexprlemrl  7611  ltexprlemfu  7612  ltexprlemru  7613  addcanprlemu  7616  recexprlemloc  7632  aptiprleml  7640  caucvgprprlemopl  7698  suplocexprlemex  7723  addclsr  7754  mulclsr  7755  recexgt0sr  7774  mulextsr1lem  7781  suplocsrlemb  7807  suplocsrlempr  7808  suplocsrlem  7809  axaddcl  7865  axaddrcl  7866  axmulcl  7867  axmulrcl  7868  axcaucvglemval  7898  subcl  8158  cru  8561  aprcl  8605  aptap  8609  divclap  8637  redivclap  8690  diveqap1bd  8795  lbinfcl  8908  cju  8920  nn1m1nn  8939  nnsub  8960  nnnn0addcl  9208  un0addcl  9211  peano2z  9291  peano2zm  9293  zaddcllemneg  9294  zaddcl  9295  nnaddm1cl  9316  nn0n0n1ge2  9325  zdivadd  9344  zdivmul  9345  suprzclex  9353  zneo  9356  peano5uzti  9363  supinfneg  9597  infsupneg  9598  qmulz  9625  qnegcl  9638  qapne  9641  qdivcl  9645  cnref1o  9652  xnegcl  9834  xltnegi  9837  xaddnemnf  9859  xaddnepnf  9860  xnegdi  9870  xnpcan  9874  xltadd1  9878  xposdif  9884  xleaddadd  9889  iccf1o  10006  ige3m2fz  10051  ige2m1fz1  10111  rebtwn2z  10257  flqcl  10275  flapcl  10277  ceilqcl  10310  intfracq  10322  modqcl  10328  mulqmod0  10332  modqdifz  10338  zmodcl  10346  modfzo0difsn  10397  modsumfzodifsn  10398  frec2uzzd  10402  frec2uzsucd  10403  frec2uzuzd  10404  frecuzrdgrrn  10410  frec2uzrdg  10411  frecuzrdgrcl  10412  frecuzrdgsuc  10416  frecuzrdgrclt  10417  frecuzrdgg  10418  frecuzrdgsuctlem  10425  fzofig  10434  iseqovex  10458  seq3val  10460  seqvalcd  10461  seqf  10463  seqovcd  10465  seq3clss  10469  seq3caopr3  10483  iseqf1olemnab  10490  iseqf1olemqk  10496  iseqf1olemjpcl  10497  iseqf1olemqpcl  10498  iseqf1olemfvp  10499  seq3f1olemqsumkj  10500  seq3f1olemqsum  10502  seq3f1oleml  10505  seq3f1o  10506  seq3distr  10515  ser0f  10517  ser3le  10520  exp3vallem  10523  exp3val  10524  exp1  10528  expcl2lemap  10534  m1expcl2  10544  expaddzap  10566  sqcl  10583  nnsqcl  10592  qsqcl  10594  zesq  10641  facp1  10712  faccl  10717  facdiv  10720  bcval  10731  bcrpcl  10735  bcp1n  10743  bcpasc  10748  permnn  10753  hashennn  10762  hashcl  10763  shftlem  10827  ovshftex  10830  shftf  10841  seq3shft  10849  cjth  10857  imval  10861  recl  10864  imcl  10865  crre  10868  remim  10871  reim0b  10873  cvg1nlemcau  10995  uzin2  10998  resqrexlem1arp  11016  resqrexlemp1rp  11017  resqrexlemglsq  11033  resqrexlemga  11034  resqrtcl  11040  abscl  11062  absrpclap  11072  nn0abscl  11096  fzomaxdiflem  11123  fzomaxdif  11124  maxabslemab  11217  maxcl  11221  zmaxcl  11235  minmax  11240  mincl  11241  xrmaxcl  11262  xrmaxaddlem  11270  xrminmax  11275  xrmincl  11276  xrmineqinf  11279  xrminrpcl  11284  reccn2ap  11323  climaddc1  11339  climmulc2  11341  climsubc1  11342  climsubc2  11343  climle  11344  climlec2  11351  climcvg1nlem  11359  sumrbdclem  11387  fsum3cvg  11388  summodclem3  11390  summodclem2a  11391  zsumdc  11394  fsumgcl  11396  fsum3  11397  isumss  11401  fisumss  11402  isumss2  11403  fsum3cvg2  11404  fsum3ser  11407  fsumcl2lem  11408  fsumcllem  11409  fsumadd  11416  sumsnf  11419  fsumsplitsn  11420  isumcl  11435  isummulc2  11436  isumrecl  11439  isumge0  11440  isumadd  11441  fsum2dlemstep  11444  fisumcom2  11448  mptfzshft  11452  fsumrev  11453  fsummulc2  11458  iserabs  11485  isumshft  11500  isumsplit  11501  isum1p  11502  isumrpcl  11504  isumle  11505  isumlessdc  11506  trireciplem  11510  expcnvap0  11512  expcnvre  11513  expcnv  11514  explecnv  11515  geolim  11521  geolim2  11522  geo2lim  11526  cvgratnnlemsumlt  11538  cvgratz  11542  mertenslemub  11544  mertenslemi1  11545  mertenslem2  11546  mertensabs  11547  prodf1f  11553  prodfdivap  11557  prodrbdclem  11581  fproddccvg  11582  prodmodclem3  11585  prodmodclem2a  11586  zproddc  11589  fprodseq  11593  fprodntrivap  11594  prodssdc  11599  fprodmul  11601  prodsnf  11602  fprodsplitdc  11606  fprodunsn  11614  fprodcl2lem  11615  fprodcllem  11616  fprodabs  11626  fprodrev  11629  fprod2dlemstep  11632  fprodcom2fi  11636  fprodsplitsn  11643  efcllemp  11668  ef0lem  11670  efcvgfsum  11677  reefcl  11678  ege2le3  11681  efcj  11683  efaddlem  11684  eftlcvg  11697  eftlcl  11698  reeftlcl  11699  eftlub  11700  efsep  11701  effsumlt  11702  efgt1p2  11705  efgt1p  11706  reeff1  11710  tanclap  11719  resincl  11730  recoscl  11731  retanclap  11732  eirraplem  11786  dvdsval2  11799  sqoddm1div8z  11893  zssinfcl  11951  infssuzex  11952  infssuzcldc  11954  zsupssdc  11957  suprzcl2dc  11958  gcdval  11962  gcdn0cl  11965  gcddvds  11966  divgcdnnr  11979  uzwodc  12040  nn0seqcvgd  12043  ialgrlem1st  12044  ialgrlemconst  12045  algrf  12047  algrp1  12048  eucalgf  12057  eucalglt  12059  lcmval  12065  lcmcllem  12069  lcmgcdlem  12079  cncongr2  12106  sqrt2irrlem  12163  oddpwdclemxy  12171  oddpwdclemdc  12175  qden1elz  12207  phicl2  12216  phimullem  12227  eulerthlemth  12234  prmdiv  12237  odzcllem  12244  pythagtriplem8  12274  pythagtriplem9  12275  pcval  12298  pczcl  12300  pcqcl  12308  dvdsprmpweqle  12338  pcaddlem  12340  pcmptcl  12342  pcmpt  12343  pockthlem  12356  pockthg  12357  zgz  12373  gznegcl  12375  gzcjcl  12376  gzaddcl  12377  gzmulcl  12378  gzabssqcl  12381  4sqlem5  12382  4sqlem4a  12391  mul4sqlem  12393  mul4sq  12394  ennnfonelemjn  12405  ennnfonelemg  12406  ennnfonelemp1  12409  ctinfomlemom  12430  ctiunctlemfo  12442  nninfdclemcl  12451  nninfdclemf  12452  nninfdclemp1  12453  setsex  12496  strsetsid  12497  ressex  12527  ressbas2d  12530  strressid  12532  tgvalex  12717  ptex  12718  prdsex  12723  imasex  12731  imasival  12732  imasbas  12733  imasplusg  12734  imasmulr  12735  imasaddfn  12743  imasaddval  12744  imasaddf  12745  imasmulfn  12746  imasmulval  12747  imasmulf  12748  qusval  12749  qusaddvallemg  12757  qusaddflemg  12758  qusaddval  12759  qusaddf  12760  qusmulval  12761  qusmulf  12762  mgm1  12794  0subm  12876  mhmeql  12881  grpsubval  12924  grplinv  12927  mulgval  12991  mulgfng  12992  mulg1  12995  mulgnnp1  12996  mulgnnsubcl  13000  mulgnn0subcl  13001  mulgsubcl  13002  mulgnndir  13017  subgex  13041  subgsubcl  13050  issubgrpd  13056  subsubg  13062  nsgconj  13071  0nsg  13079  triv1nsgd  13083  eqger  13088  eqgcpbl  13092  mgpex  13140  mgpf  13199  opprex  13250  opprring  13254  dvdsrex  13272  opprunitd  13284  dvrvald  13308  dvrcl  13309  unitdvcl  13310  invrpropdg  13323  subrgcrng  13351  subrgsubm  13360  subrgugrp  13366  subsubrg  13371  aprcotr  13380  rmodislmod  13446  lssvsubcl  13457  islss3  13471  cnsubglem  13512  iunopn  13541  toponmax  13564  tgtop  13607  tgiun  13612  tgidm  13613  ntropn  13656  tgrest  13708  restopnb  13720  cnovex  13735  cnclima  13762  txvalex  13793  txtop  13799  tx1cn  13808  tx2cn  13809  txcnp  13810  txcnmpt  13812  txdis1cn  13817  cnmptcom  13837  imasnopn  13838  hmeocnv  13846  hmeores  13854  txhmeo  13858  txswaphmeo  13860  ispsmet  13862  xmetres  13921  metres  13922  blex  13926  xmeter  13975  xmetresbl  13979  mopntopon  13982  isxms2  13991  xmetxp  14046  xmettx  14049  txmetcnp  14057  qtopbasss  14060  qtopbas  14061  reopnap  14077  ioo2blex  14083  blssioo  14084  tgioo  14085  fsumcncntop  14095  cncfval  14098  divccncfap  14116  cdivcncfap  14126  ivthdec  14161  limccnpcntop  14183  dvrecap  14216  pilem3  14243  tanrpcl  14297  cosordlem  14309  ioocosf1o  14314  rpcncxpcl  14362  rpcxpcl  14363  rpabscxpbnd  14398  rplogbcl  14403  lgslem1  14440  lgsval  14444  lgscllem  14447  lgsne0  14478  lgseisenlem1  14489  2sqlem3  14503  2sqlem8  14509  djucllem  14591  012of  14784  2o01f  14785  nninfsellemeq  14802  qdencn  14814  cvgcmp2nlemabs  14819  trilpolemclim  14823  trilpolemisumle  14825  trilpolemeq1  14827  trilpolemlt1  14828  nconstwlpolemgt0  14851