Theorem eqeltrd 2234

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

Syntax hints:   → wi 4   = wceq 1335   ∈ wcel 2128

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-4 1490  ax-17 1506  ax-ial 1514  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-cleq 2150  df-clel 2153

This theorem is referenced by:  eqeltrrd  2235  3eltr4d  2241  eqeltrid  2244  eqeltrdi  2248  ifcldadc  3534  ifcldcd  3540  intab  3836  disjiun  3960  iinexgm  4115  opexg  4188  tfisi  4545  nnpredcl  4581  imain  5251  fvmptd  5548  fvmptdf  5554  fvmptt  5558  elfvmptrab  5562  dffo3  5613  resfunexg  5687  f1oiso2  5774  riota2df  5797  riota5f  5801  ovmpodxf  5943  ovmpodf  5949  offval  6036  ofvalg  6038  offeq  6042  iunexg  6064  oprabexd  6072  fo1stresm  6106  fo2ndresm  6107  oprssdmm  6116  1stdm  6127  1stconst  6165  2ndconst  6166  cnvf1olem  6168  fo2ndf  6171  f1od2  6179  iunon  6228  tfrlemibacc  6270  tfrlemibfn  6272  tfr1onlembacc  6286  tfr1onlembfn  6288  tfrcllembacc  6299  tfrcllembfn  6301  tfrcl  6308  rdgon  6330  frec0g  6341  freccllem  6346  frecfcllem  6348  frecsuclem  6350  oacl  6404  omcl  6405  oeicl  6406  nntr2  6447  mptelixpg  6676  fidifsnen  6812  en2eqpr  6849  unfiin  6867  ssfirab  6875  fnfi  6878  relcnvfi  6882  fidcenumlemr  6896  elfi2  6913  supclti  6938  supubti  6939  suplubti  6940  supelti  6942  ordiso2  6973  djulclr  6987  djurclr  6988  djulcl  6989  djurcl  6990  djuss  7008  updjudhcoinlf  7018  updjudhcoinrg  7019  ctssdclemn0  7048  ctssdccl  7049  ctssdc  7051  enumctlemm  7052  cardcl  7110  exmidontriimlem2  7151  cc2lem  7180  cc3  7182  addclpi  7241  mulclpi  7242  addclnq  7289  mulclnq  7290  addclnq0  7365  mulclnq0  7366  nqpnq0nq  7367  elnp1st2nd  7390  prarloclemcalc  7416  distrlem1prl  7496  distrlem1pru  7497  ltexprlemopl  7515  ltexprlemopu  7517  ltexprlemfl  7523  ltexprlemrl  7524  ltexprlemfu  7525  ltexprlemru  7526  addcanprlemu  7529  recexprlemloc  7545  aptiprleml  7553  caucvgprprlemopl  7611  suplocexprlemex  7636  addclsr  7667  mulclsr  7668  recexgt0sr  7687  mulextsr1lem  7694  suplocsrlemb  7720  suplocsrlempr  7721  suplocsrlem  7722  axaddcl  7778  axaddrcl  7779  axmulcl  7780  axmulrcl  7781  axcaucvglemval  7811  subcl  8068  cru  8471  aprcl  8515  divclap  8545  redivclap  8598  diveqap1bd  8702  lbinfcl  8814  cju  8826  nn1m1nn  8845  nnsub  8866  nnnn0addcl  9114  un0addcl  9117  peano2z  9197  peano2zm  9199  zaddcllemneg  9200  zaddcl  9201  nnaddm1cl  9222  nn0n0n1ge2  9228  zdivadd  9247  zdivmul  9248  suprzclex  9256  zneo  9259  peano5uzti  9266  supinfneg  9500  infsupneg  9501  qmulz  9525  qnegcl  9538  qapne  9541  qdivcl  9545  cnref1o  9552  xnegcl  9729  xltnegi  9732  xaddnemnf  9754  xaddnepnf  9755  xnegdi  9765  xnpcan  9769  xltadd1  9773  xposdif  9779  xleaddadd  9784  iccf1o  9901  ige3m2fz  9944  ige2m1fz1  10004  rebtwn2z  10147  flqcl  10165  flapcl  10167  ceilqcl  10200  intfracq  10212  modqcl  10218  mulqmod0  10222  modqdifz  10228  zmodcl  10236  modfzo0difsn  10287  modsumfzodifsn  10288  frec2uzzd  10292  frec2uzsucd  10293  frec2uzuzd  10294  frecuzrdgrrn  10300  frec2uzrdg  10301  frecuzrdgrcl  10302  frecuzrdgsuc  10306  frecuzrdgrclt  10307  frecuzrdgg  10308  frecuzrdgsuctlem  10315  fzofig  10324  iseqovex  10348  seq3val  10350  seqvalcd  10351  seqf  10353  seqovcd  10355  seq3clss  10359  seq3caopr3  10373  iseqf1olemnab  10380  iseqf1olemqk  10386  iseqf1olemjpcl  10387  iseqf1olemqpcl  10388  iseqf1olemfvp  10389  seq3f1olemqsumkj  10390  seq3f1olemqsum  10392  seq3f1oleml  10395  seq3f1o  10396  seq3distr  10405  ser0f  10407  ser3le  10410  exp3vallem  10413  exp3val  10414  exp1  10418  expcl2lemap  10424  m1expcl2  10434  expaddzap  10456  sqcl  10473  nnsqcl  10481  qsqcl  10483  zesq  10529  facp1  10597  faccl  10602  facdiv  10605  bcval  10616  bcrpcl  10620  bcp1n  10628  bcpasc  10633  permnn  10638  hashennn  10647  hashcl  10648  shftlem  10709  ovshftex  10712  shftf  10723  seq3shft  10731  cjth  10739  imval  10743  recl  10746  imcl  10747  crre  10750  remim  10753  reim0b  10755  cvg1nlemcau  10877  uzin2  10880  resqrexlem1arp  10898  resqrexlemp1rp  10899  resqrexlemglsq  10915  resqrexlemga  10916  resqrtcl  10922  abscl  10944  absrpclap  10954  nn0abscl  10978  fzomaxdiflem  11005  fzomaxdif  11006  maxabslemab  11099  maxcl  11103  zmaxcl  11117  minmax  11122  mincl  11123  xrmaxcl  11142  xrmaxaddlem  11150  xrminmax  11155  xrmincl  11156  xrmineqinf  11159  xrminrpcl  11164  reccn2ap  11203  climaddc1  11219  climmulc2  11221  climsubc1  11222  climsubc2  11223  climle  11224  climlec2  11231  climcvg1nlem  11239  sumrbdclem  11267  fsum3cvg  11268  summodclem3  11270  summodclem2a  11271  zsumdc  11274  fsumgcl  11276  fsum3  11277  isumss  11281  fisumss  11282  isumss2  11283  fsum3cvg2  11284  fsum3ser  11287  fsumcl2lem  11288  fsumcllem  11289  fsumadd  11296  sumsnf  11299  fsumsplitsn  11300  isumcl  11315  isummulc2  11316  isumrecl  11319  isumge0  11320  isumadd  11321  fsum2dlemstep  11324  fisumcom2  11328  mptfzshft  11332  fsumrev  11333  fsummulc2  11338  iserabs  11365  isumshft  11380  isumsplit  11381  isum1p  11382  isumrpcl  11384  isumle  11385  isumlessdc  11386  trireciplem  11390  expcnvap0  11392  expcnvre  11393  expcnv  11394  explecnv  11395  geolim  11401  geolim2  11402  geo2lim  11406  cvgratnnlemsumlt  11418  cvgratz  11422  mertenslemub  11424  mertenslemi1  11425  mertenslem2  11426  mertensabs  11427  prodf1f  11433  prodfdivap  11437  prodrbdclem  11461  fproddccvg  11462  prodmodclem3  11465  prodmodclem2a  11466  zproddc  11469  fprodseq  11473  fprodntrivap  11474  prodssdc  11479  fprodmul  11481  prodsnf  11482  fprodsplitdc  11486  fprodunsn  11494  fprodcl2lem  11495  fprodcllem  11496  fprodabs  11506  fprodrev  11509  fprod2dlemstep  11512  fprodcom2fi  11516  fprodsplitsn  11523  efcllemp  11548  ef0lem  11550  efcvgfsum  11557  reefcl  11558  ege2le3  11561  efcj  11563  efaddlem  11564  eftlcvg  11577  eftlcl  11578  reeftlcl  11579  eftlub  11580  efsep  11581  effsumlt  11582  efgt1p2  11585  efgt1p  11586  reeff1  11590  tanclap  11599  resincl  11610  recoscl  11611  retanclap  11612  eirraplem  11666  dvdsval2  11679  sqoddm1div8z  11769  zssinfcl  11827  infssuzex  11828  infssuzcldc  11830  gcdval  11834  gcdn0cl  11837  gcddvds  11838  divgcdnnr  11851  nn0seqcvgd  11909  ialgrlem1st  11910  ialgrlemconst  11911  algrf  11913  algrp1  11914  eucalgf  11923  eucalglt  11925  lcmval  11931  lcmcllem  11935  lcmgcdlem  11945  cncongr2  11972  sqrt2irrlem  12026  oddpwdclemxy  12034  oddpwdclemdc  12038  qden1elz  12070  phicl2  12077  phimullem  12088  eulerthlemth  12095  prmdiv  12098  ennnfonelemjn  12114  ennnfonelemg  12115  ennnfonelemp1  12118  ctinfomlemom  12139  ctiunctlemfo  12151  setsex  12193  strsetsid  12194  ressid2  12220  ressval2  12221  ressid  12222  iunopn  12371  toponmax  12394  tgvalex  12421  tgtop  12439  tgiun  12444  tgidm  12445  ntropn  12488  tgrest  12540  restopnb  12552  cnovex  12567  cnclima  12594  txvalex  12625  txtop  12631  tx1cn  12640  tx2cn  12641  txcnp  12642  txcnmpt  12644  txdis1cn  12649  cnmptcom  12669  imasnopn  12670  hmeocnv  12678  hmeores  12686  txhmeo  12690  txswaphmeo  12692  ispsmet  12694  xmetres  12753  metres  12754  blex  12758  xmeter  12807  xmetresbl  12811  mopntopon  12814  isxms2  12823  xmetxp  12878  xmettx  12881  txmetcnp  12889  qtopbasss  12892  qtopbas  12893  reopnap  12909  ioo2blex  12915  blssioo  12916  tgioo  12917  fsumcncntop  12927  cncfval  12930  divccncfap  12948  cdivcncfap  12958  ivthdec  12993  limccnpcntop  13015  dvrecap  13048  pilem3  13075  tanrpcl  13129  cosordlem  13141  ioocosf1o  13146  rpcncxpcl  13194  rpcxpcl  13195  rpabscxpbnd  13230  rplogbcl  13234  djucllem  13345  012of  13538  2o01f  13539  nninfsellemeq  13557  qdencn  13569  cvgcmp2nlemabs  13574  trilpolemclim  13578  trilpolemisumle  13580  trilpolemeq1  13582  trilpolemlt1  13583  nconstwlpolemgt0  13605