Theorem eqeltrd 2247

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

Syntax hints:   → wi 4   = wceq 1348   ∈ wcel 2141

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 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-clel 2166

This theorem is referenced by:  eqeltrrd  2248  3eltr4d  2254  eqeltrid  2257  eqeltrdi  2261  ifcldadc  3555  ifcldcd  3561  intab  3860  disjiun  3984  iinexgm  4140  opexg  4213  tfisi  4571  nnpredcl  4607  imain  5280  fvmptd  5577  fvmptdf  5583  fvmptt  5587  elfvmptrab  5591  dffo3  5643  resfunexg  5717  f1oiso2  5806  riota2df  5829  riota5f  5833  ovmpodxf  5978  ovmpodf  5984  offval  6068  ofvalg  6070  offeq  6074  iunexg  6098  oprabexd  6106  fo1stresm  6140  fo2ndresm  6141  oprssdmm  6150  1stdm  6161  1stconst  6200  2ndconst  6201  cnvf1olem  6203  fo2ndf  6206  f1od2  6214  iunon  6263  tfrlemibacc  6305  tfrlemibfn  6307  tfr1onlembacc  6321  tfr1onlembfn  6323  tfrcllembacc  6334  tfrcllembfn  6336  tfrcl  6343  rdgon  6365  frec0g  6376  freccllem  6381  frecfcllem  6383  frecsuclem  6385  oacl  6439  omcl  6440  oeicl  6441  nntr2  6482  mptelixpg  6712  fidifsnen  6848  en2eqpr  6885  unfiin  6903  ssfirab  6911  fnfi  6914  relcnvfi  6918  fidcenumlemr  6932  elfi2  6949  supclti  6975  supubti  6976  suplubti  6977  supelti  6979  ordiso2  7012  djulclr  7026  djurclr  7027  djulcl  7028  djurcl  7029  djuss  7047  updjudhcoinlf  7057  updjudhcoinrg  7058  ctssdclemn0  7087  ctssdccl  7088  ctssdc  7090  enumctlemm  7091  nninfwlpoimlemg  7151  cardcl  7158  exmidontriimlem2  7199  cc2lem  7228  cc3  7230  addclpi  7289  mulclpi  7290  addclnq  7337  mulclnq  7338  addclnq0  7413  mulclnq0  7414  nqpnq0nq  7415  elnp1st2nd  7438  prarloclemcalc  7464  distrlem1prl  7544  distrlem1pru  7545  ltexprlemopl  7563  ltexprlemopu  7565  ltexprlemfl  7571  ltexprlemrl  7572  ltexprlemfu  7573  ltexprlemru  7574  addcanprlemu  7577  recexprlemloc  7593  aptiprleml  7601  caucvgprprlemopl  7659  suplocexprlemex  7684  addclsr  7715  mulclsr  7716  recexgt0sr  7735  mulextsr1lem  7742  suplocsrlemb  7768  suplocsrlempr  7769  suplocsrlem  7770  axaddcl  7826  axaddrcl  7827  axmulcl  7828  axmulrcl  7829  axcaucvglemval  7859  subcl  8118  cru  8521  aprcl  8565  divclap  8595  redivclap  8648  diveqap1bd  8753  lbinfcl  8865  cju  8877  nn1m1nn  8896  nnsub  8917  nnnn0addcl  9165  un0addcl  9168  peano2z  9248  peano2zm  9250  zaddcllemneg  9251  zaddcl  9252  nnaddm1cl  9273  nn0n0n1ge2  9282  zdivadd  9301  zdivmul  9302  suprzclex  9310  zneo  9313  peano5uzti  9320  supinfneg  9554  infsupneg  9555  qmulz  9582  qnegcl  9595  qapne  9598  qdivcl  9602  cnref1o  9609  xnegcl  9789  xltnegi  9792  xaddnemnf  9814  xaddnepnf  9815  xnegdi  9825  xnpcan  9829  xltadd1  9833  xposdif  9839  xleaddadd  9844  iccf1o  9961  ige3m2fz  10005  ige2m1fz1  10065  rebtwn2z  10211  flqcl  10229  flapcl  10231  ceilqcl  10264  intfracq  10276  modqcl  10282  mulqmod0  10286  modqdifz  10292  zmodcl  10300  modfzo0difsn  10351  modsumfzodifsn  10352  frec2uzzd  10356  frec2uzsucd  10357  frec2uzuzd  10358  frecuzrdgrrn  10364  frec2uzrdg  10365  frecuzrdgrcl  10366  frecuzrdgsuc  10370  frecuzrdgrclt  10371  frecuzrdgg  10372  frecuzrdgsuctlem  10379  fzofig  10388  iseqovex  10412  seq3val  10414  seqvalcd  10415  seqf  10417  seqovcd  10419  seq3clss  10423  seq3caopr3  10437  iseqf1olemnab  10444  iseqf1olemqk  10450  iseqf1olemjpcl  10451  iseqf1olemqpcl  10452  iseqf1olemfvp  10453  seq3f1olemqsumkj  10454  seq3f1olemqsum  10456  seq3f1oleml  10459  seq3f1o  10460  seq3distr  10469  ser0f  10471  ser3le  10474  exp3vallem  10477  exp3val  10478  exp1  10482  expcl2lemap  10488  m1expcl2  10498  expaddzap  10520  sqcl  10537  nnsqcl  10545  qsqcl  10547  zesq  10594  facp1  10664  faccl  10669  facdiv  10672  bcval  10683  bcrpcl  10687  bcp1n  10695  bcpasc  10700  permnn  10705  hashennn  10714  hashcl  10715  shftlem  10780  ovshftex  10783  shftf  10794  seq3shft  10802  cjth  10810  imval  10814  recl  10817  imcl  10818  crre  10821  remim  10824  reim0b  10826  cvg1nlemcau  10948  uzin2  10951  resqrexlem1arp  10969  resqrexlemp1rp  10970  resqrexlemglsq  10986  resqrexlemga  10987  resqrtcl  10993  abscl  11015  absrpclap  11025  nn0abscl  11049  fzomaxdiflem  11076  fzomaxdif  11077  maxabslemab  11170  maxcl  11174  zmaxcl  11188  minmax  11193  mincl  11194  xrmaxcl  11215  xrmaxaddlem  11223  xrminmax  11228  xrmincl  11229  xrmineqinf  11232  xrminrpcl  11237  reccn2ap  11276  climaddc1  11292  climmulc2  11294  climsubc1  11295  climsubc2  11296  climle  11297  climlec2  11304  climcvg1nlem  11312  sumrbdclem  11340  fsum3cvg  11341  summodclem3  11343  summodclem2a  11344  zsumdc  11347  fsumgcl  11349  fsum3  11350  isumss  11354  fisumss  11355  isumss2  11356  fsum3cvg2  11357  fsum3ser  11360  fsumcl2lem  11361  fsumcllem  11362  fsumadd  11369  sumsnf  11372  fsumsplitsn  11373  isumcl  11388  isummulc2  11389  isumrecl  11392  isumge0  11393  isumadd  11394  fsum2dlemstep  11397  fisumcom2  11401  mptfzshft  11405  fsumrev  11406  fsummulc2  11411  iserabs  11438  isumshft  11453  isumsplit  11454  isum1p  11455  isumrpcl  11457  isumle  11458  isumlessdc  11459  trireciplem  11463  expcnvap0  11465  expcnvre  11466  expcnv  11467  explecnv  11468  geolim  11474  geolim2  11475  geo2lim  11479  cvgratnnlemsumlt  11491  cvgratz  11495  mertenslemub  11497  mertenslemi1  11498  mertenslem2  11499  mertensabs  11500  prodf1f  11506  prodfdivap  11510  prodrbdclem  11534  fproddccvg  11535  prodmodclem3  11538  prodmodclem2a  11539  zproddc  11542  fprodseq  11546  fprodntrivap  11547  prodssdc  11552  fprodmul  11554  prodsnf  11555  fprodsplitdc  11559  fprodunsn  11567  fprodcl2lem  11568  fprodcllem  11569  fprodabs  11579  fprodrev  11582  fprod2dlemstep  11585  fprodcom2fi  11589  fprodsplitsn  11596  efcllemp  11621  ef0lem  11623  efcvgfsum  11630  reefcl  11631  ege2le3  11634  efcj  11636  efaddlem  11637  eftlcvg  11650  eftlcl  11651  reeftlcl  11652  eftlub  11653  efsep  11654  effsumlt  11655  efgt1p2  11658  efgt1p  11659  reeff1  11663  tanclap  11672  resincl  11683  recoscl  11684  retanclap  11685  eirraplem  11739  dvdsval2  11752  sqoddm1div8z  11845  zssinfcl  11903  infssuzex  11904  infssuzcldc  11906  zsupssdc  11909  suprzcl2dc  11910  gcdval  11914  gcdn0cl  11917  gcddvds  11918  divgcdnnr  11931  uzwodc  11992  nn0seqcvgd  11995  ialgrlem1st  11996  ialgrlemconst  11997  algrf  11999  algrp1  12000  eucalgf  12009  eucalglt  12011  lcmval  12017  lcmcllem  12021  lcmgcdlem  12031  cncongr2  12058  sqrt2irrlem  12115  oddpwdclemxy  12123  oddpwdclemdc  12127  qden1elz  12159  phicl2  12168  phimullem  12179  eulerthlemth  12186  prmdiv  12189  odzcllem  12196  pythagtriplem8  12226  pythagtriplem9  12227  pcval  12250  pczcl  12252  pcqcl  12260  dvdsprmpweqle  12290  pcaddlem  12292  pcmptcl  12294  pcmpt  12295  pockthlem  12308  pockthg  12309  zgz  12325  gznegcl  12327  gzcjcl  12328  gzaddcl  12329  gzmulcl  12330  gzabssqcl  12333  4sqlem5  12334  4sqlem4a  12343  mul4sqlem  12345  mul4sq  12346  ennnfonelemjn  12357  ennnfonelemg  12358  ennnfonelemp1  12361  ctinfomlemom  12382  ctiunctlemfo  12394  nninfdclemcl  12403  nninfdclemf  12404  nninfdclemp1  12405  setsex  12448  strsetsid  12449  ressid2  12477  ressval2  12478  ressid  12479  mgm1  12624  0subm  12702  mhmeql  12707  grpsubval  12749  grplinv  12752  iunopn  12794  toponmax  12817  tgvalex  12844  tgtop  12862  tgiun  12867  tgidm  12868  ntropn  12911  tgrest  12963  restopnb  12975  cnovex  12990  cnclima  13017  txvalex  13048  txtop  13054  tx1cn  13063  tx2cn  13064  txcnp  13065  txcnmpt  13067  txdis1cn  13072  cnmptcom  13092  imasnopn  13093  hmeocnv  13101  hmeores  13109  txhmeo  13113  txswaphmeo  13115  ispsmet  13117  xmetres  13176  metres  13177  blex  13181  xmeter  13230  xmetresbl  13234  mopntopon  13237  isxms2  13246  xmetxp  13301  xmettx  13304  txmetcnp  13312  qtopbasss  13315  qtopbas  13316  reopnap  13332  ioo2blex  13338  blssioo  13339  tgioo  13340  fsumcncntop  13350  cncfval  13353  divccncfap  13371  cdivcncfap  13381  ivthdec  13416  limccnpcntop  13438  dvrecap  13471  pilem3  13498  tanrpcl  13552  cosordlem  13564  ioocosf1o  13569  rpcncxpcl  13617  rpcxpcl  13618  rpabscxpbnd  13653  rplogbcl  13658  lgslem1  13695  lgsval  13699  lgscllem  13702  lgsne0  13733  2sqlem3  13747  2sqlem8  13753  djucllem  13835  012of  14028  2o01f  14029  nninfsellemeq  14047  qdencn  14059  cvgcmp2nlemabs  14064  trilpolemclim  14068  trilpolemisumle  14070  trilpolemeq1  14072  trilpolemlt1  14073  nconstwlpolemgt0  14095