Theorem eqeltrd 2308

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

Syntax hints:   → wi 4   = wceq 1397   ∈ wcel 2202

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227

This theorem is referenced by:  eqeltrrd  2309  3eltr4d  2315  eqeltrid  2318  eqeltrdi  2322  ifcldadc  3635  ifcldcd  3643  intab  3957  disjiun  4083  iinexgm  4244  opexg  4320  tfisi  4685  nnpredcl  4721  opabssxpd  4762  imain  5412  fvmptd  5727  fvmptdf  5734  fvmptt  5738  elfvmptrab  5742  dffo3  5794  resfunexg  5875  f1oiso2  5968  riota2df  5993  riota5f  5998  ovmpodxf  6147  ovmpodf  6153  offval  6243  ofvalg  6245  offeq  6249  iunexg  6281  oprabexd  6289  fo1stresm  6324  fo2ndresm  6325  oprssdmm  6334  1stdm  6345  1stconst  6386  2ndconst  6387  cnvf1olem  6389  fo2ndf  6392  f1od2  6400  iunon  6450  tfrlemibacc  6492  tfrlemibfn  6494  tfr1onlembacc  6508  tfr1onlembfn  6510  tfrcllembacc  6521  tfrcllembfn  6523  tfrcl  6530  rdgon  6552  frec0g  6563  freccllem  6568  frecfcllem  6570  frecsuclem  6572  oacl  6628  omcl  6629  oeicl  6630  nntr2  6671  mptelixpg  6903  fidifsnen  7057  en2eqpr  7099  unfiin  7118  tpfidceq  7122  ssfirab  7129  fnfi  7135  relcnvfi  7140  fidcenumlemr  7154  elfi2  7171  supclti  7197  supubti  7198  suplubti  7199  supelti  7201  ordiso2  7234  djulclr  7248  djurclr  7249  djulcl  7250  djurcl  7251  djuss  7269  updjudhcoinlf  7279  updjudhcoinrg  7280  ctssdclemn0  7309  ctssdccl  7310  ctssdc  7312  enumctlemm  7313  nninfwlpoimlemg  7374  cardcl  7385  exmidontriimlem2  7437  exmidapne  7479  cc2lem  7485  cc3  7487  addclpi  7547  mulclpi  7548  addclnq  7595  mulclnq  7596  addclnq0  7671  mulclnq0  7672  nqpnq0nq  7673  elnp1st2nd  7696  prarloclemcalc  7722  distrlem1prl  7802  distrlem1pru  7803  ltexprlemopl  7821  ltexprlemopu  7823  ltexprlemfl  7829  ltexprlemrl  7830  ltexprlemfu  7831  ltexprlemru  7832  addcanprlemu  7835  recexprlemloc  7851  aptiprleml  7859  caucvgprprlemopl  7917  suplocexprlemex  7942  addclsr  7973  mulclsr  7974  recexgt0sr  7993  mulextsr1lem  8000  suplocsrlemb  8026  suplocsrlempr  8027  suplocsrlem  8028  axaddcl  8084  axaddrcl  8085  axmulcl  8086  axmulrcl  8087  axcaucvglemval  8117  subcl  8378  cru  8782  aprcl  8826  aptap  8830  divclap  8858  redivclap  8911  diveqap1bd  9016  lbinfcl  9129  cju  9141  nn1m1nn  9161  nnsub  9182  nnnn0addcl  9432  un0addcl  9435  peano2z  9515  peano2zm  9517  zaddcllemneg  9518  zaddcl  9519  nnaddm1cl  9541  nn0n0n1ge2  9550  zdivadd  9569  zdivmul  9570  suprzclex  9578  zneo  9581  peano5uzti  9588  supinfneg  9829  infsupneg  9830  qmulz  9857  qnegcl  9870  qapne  9873  qdivcl  9877  cnref1o  9885  xnegcl  10067  xltnegi  10070  xaddnemnf  10092  xaddnepnf  10093  xnegdi  10103  xnpcan  10107  xltadd1  10111  xposdif  10117  xleaddadd  10122  iccf1o  10239  ige3m2fz  10284  ige2m1fz1  10344  zssinfcl  10493  infssuzex  10494  infssuzcldc  10496  zsupssdc  10499  suprzcl2dc  10500  rebtwn2z  10515  flqcl  10534  flapcl  10536  ceilqcl  10571  intfracq  10583  modqcl  10589  mulqmod0  10593  modqdifz  10599  zmodcl  10607  modfzo0difsn  10658  modsumfzodifsn  10659  frec2uzzd  10663  frec2uzsucd  10664  frec2uzuzd  10665  frecuzrdgrrn  10671  frec2uzrdg  10672  frecuzrdgrcl  10673  frecuzrdgsuc  10677  frecuzrdgrclt  10678  frecuzrdgg  10679  frecuzrdgsuctlem  10686  fzofig  10695  iseqovex  10721  seq3val  10723  seqvalcd  10724  seqf  10727  seqovcd  10730  seq3clss  10734  seq3caopr3  10754  iseqf1olemnab  10764  iseqf1olemqk  10770  iseqf1olemjpcl  10771  iseqf1olemqpcl  10772  iseqf1olemfvp  10773  seq3f1olemqsumkj  10774  seq3f1olemqsum  10776  seq3f1oleml  10779  seq3f1o  10780  seqf1oglem2a  10781  seqf1oglem1  10782  seqf1oglem2  10783  seq3distr  10795  ser0f  10797  ser3le  10800  exp3vallem  10803  exp3val  10804  exp1  10808  expcl2lemap  10814  m1expcl2  10824  expaddzap  10846  sqcl  10863  nnsqcl  10872  qsqcl  10874  zesq  10921  facp1  10993  faccl  10998  facdiv  11001  bcval  11012  bcrpcl  11016  bcp1n  11024  bcpasc  11029  permnn  11034  hashennn  11043  hashcl  11044  lencl  11121  wrdexg  11128  elovmpowrd  11159  lswcl  11168  ccatcl  11174  ccatrn  11190  lswccatn0lsw  11192  ccatalpha  11194  s1cl  11202  swrdclg  11235  swrdwrdsymbg  11249  ccatswrd  11255  pfxval  11259  fnpfx  11262  pfxclg  11263  pfxwrdsymbg  11275  ccatpfx  11286  lenrevpfxcctswrd  11297  wrdind  11307  wrd2ind  11308  shftlem  11394  ovshftex  11397  shftf  11408  seq3shft  11416  cjth  11424  imval  11428  recl  11431  imcl  11432  crre  11435  remim  11438  reim0b  11440  cvg1nlemcau  11562  uzin2  11565  resqrexlem1arp  11583  resqrexlemp1rp  11584  resqrexlemglsq  11600  resqrexlemga  11601  resqrtcl  11607  abscl  11629  absrpclap  11639  nn0abscl  11663  fzomaxdiflem  11690  fzomaxdif  11691  maxabslemab  11784  maxcl  11788  zmaxcl  11802  minmax  11808  mincl  11809  xrmaxcl  11830  xrmaxaddlem  11838  xrminmax  11843  xrmincl  11844  xrmineqinf  11847  xrminrpcl  11852  reccn2ap  11891  climaddc1  11907  climmulc2  11909  climsubc1  11910  climsubc2  11911  climle  11912  climlec2  11919  climcvg1nlem  11927  sumrbdclem  11956  fsum3cvg  11957  summodclem3  11959  summodclem2a  11960  zsumdc  11963  fsumgcl  11965  fsum3  11966  isumss  11970  fisumss  11971  isumss2  11972  fsum3cvg2  11973  fsum3ser  11976  fsumcl2lem  11977  fsumcllem  11978  fsumadd  11985  sumsnf  11988  fsumsplitsn  11989  isumcl  12004  isummulc2  12005  isumrecl  12008  isumge0  12009  isumadd  12010  fsum2dlemstep  12013  fisumcom2  12017  mptfzshft  12021  fsumrev  12022  fsummulc2  12027  iserabs  12054  isumshft  12069  isumsplit  12070  isum1p  12071  isumrpcl  12073  isumle  12074  isumlessdc  12075  trireciplem  12079  expcnvap0  12081  expcnvre  12082  expcnv  12083  explecnv  12084  geolim  12090  geolim2  12091  geo2lim  12095  cvgratnnlemsumlt  12107  cvgratz  12111  mertenslemub  12113  mertenslemi1  12114  mertenslem2  12115  mertensabs  12116  prodf1f  12122  prodfdivap  12126  prodrbdclem  12150  fproddccvg  12151  prodmodclem3  12154  prodmodclem2a  12155  zproddc  12158  fprodseq  12162  fprodntrivap  12163  prodssdc  12168  fprodmul  12170  prodsnf  12171  fprodsplitdc  12175  fprodunsn  12183  fprodcl2lem  12184  fprodcllem  12185  fprodabs  12195  fprodrev  12198  fprod2dlemstep  12201  fprodcom2fi  12205  fprodsplitsn  12212  efcllemp  12237  ef0lem  12239  efcvgfsum  12246  reefcl  12247  ege2le3  12250  efcj  12252  efaddlem  12253  eftlcvg  12266  eftlcl  12267  reeftlcl  12268  eftlub  12269  efsep  12270  effsumlt  12271  efgt1p2  12274  efgt1p  12275  reeff1  12279  tanclap  12288  resincl  12299  recoscl  12300  retanclap  12301  eirraplem  12356  dvdsval2  12369  fsumdvds  12421  sqoddm1div8z  12465  bitsinv1lem  12540  gcdval  12548  gcdn0cl  12551  gcddvds  12552  divgcdnnr  12565  uzwodc  12626  nn0seqcvgd  12631  ialgrlem1st  12632  ialgrlemconst  12633  algrf  12635  algrp1  12636  eucalgf  12645  eucalglt  12647  lcmval  12653  lcmcllem  12657  lcmgcdlem  12667  cncongr2  12694  sqrt2irrlem  12751  oddpwdclemxy  12759  oddpwdclemdc  12763  qden1elz  12795  phicl2  12804  phimullem  12815  eulerthlemth  12822  prmdiv  12825  odzcllem  12833  pythagtriplem8  12863  pythagtriplem9  12864  pcval  12887  pczcl  12889  pcqcl  12897  dvdsprmpweqle  12928  pcaddlem  12930  pcmptcl  12933  pcmpt  12934  pockthlem  12947  pockthg  12948  zgz  12964  gznegcl  12966  gzcjcl  12967  gzaddcl  12968  gzmulcl  12969  gzabssqcl  12972  4sqlem5  12973  4sqlem4a  12982  mul4sqlem  12984  mul4sq  12985  4sqlemafi  12986  4sqlemffi  12987  4sqleminfi  12988  4sqexercise1  12989  4sqlem16  12997  4sqlem17  12998  ennnfonelemjn  13041  ennnfonelemg  13042  ennnfonelemp1  13045  ctinfomlemom  13066  ctiunctlemfo  13078  nninfdclemcl  13087  nninfdclemf  13088  nninfdclemp1  13089  setsex  13132  strsetsid  13133  strslfv3  13146  bassetsnn  13157  ressex  13166  ressbas2d  13169  strressid  13172  tgvalex  13364  ptex  13365  prdsex  13370  prdsval  13374  imasex  13406  imasival  13407  imasbas  13408  imasplusg  13409  imasmulr  13410  imasaddfn  13418  imasaddval  13419  imasaddf  13420  imasmulfn  13421  imasmulval  13422  imasmulf  13423  qusval  13424  qusex  13426  qusaddvallemg  13434  qusaddflemg  13435  qusaddval  13436  qusaddf  13437  qusmulval  13438  qusmulf  13439  mgm1  13471  gsumress  13496  gsumprval  13500  prdsplusgsgrpcl  13515  prdsplusgcl  13547  prdsidlem  13548  pwsmnd  13551  mhmex  13563  subsubm  13584  0subm  13585  mhmeql  13593  gsumwsubmcl  13597  gsumfzcl  13600  grpsubval  13647  grplinv  13651  pwsgrp  13712  qusgrp2  13718  mulgval  13727  mulgex  13728  mulgfng  13729  mulg1  13734  mulgnnp1  13735  mulgnnsubcl  13739  mulgnn0subcl  13740  mulgsubcl  13741  mulgnndir  13756  subgex  13781  subgsubcl  13790  issubgrpd  13796  subsubg  13802  nsgconj  13811  0nsg  13819  triv1nsgd  13823  eqgex  13826  eqger  13829  eqgcpbl  13833  ghmex  13860  ghmpreima  13871  ghmnsgpreima  13874  conjnmz  13884  gsumfzsubmcl  13943  gsumsplit0  13951  mgpex  13957  rngmgpf  13969  qusrng  13990  mgpf  14043  qusring2  14098  opprex  14105  opprrng  14109  opprring  14111  dvdsrex  14131  opprunitd  14143  dvrvald  14167  dvrcl  14168  unitdvcl  14169  invrpropdg  14182  subsubrng  14247  subrgcrng  14258  subrgsubm  14267  subrgugrp  14273  subsubrg  14278  rnrhmsubrg  14285  aprcotr  14318  rmodislmod  14384  lssvsubcl  14399  islss3  14412  lspex  14428  ellspsn  14450  sraex  14479  rlmlmod  14497  lidlex  14506  rspex  14507  lidl0cl  14516  lidlacl  14517  lidlnegcl  14518  ridl0  14543  ridl1  14544  2idlelbas  14549  cnsubglem  14612  expghmap  14640  mulgrhm  14642  zrhex  14654  znbaslemnn  14672  psrval  14699  psrbagfi  14706  psrbasg  14707  mplsubgfilemm  14731  mplsubgfilemcl  14732  mplsubgfileminv  14733  mplgrpfi  14739  iunopn  14745  toponmax  14768  tgtop  14811  tgiun  14816  tgidm  14817  ntropn  14860  tgrest  14912  restopnb  14924  cnovex  14939  cnclima  14966  txvalex  14997  txtop  15003  tx1cn  15012  tx2cn  15013  txcnp  15014  txcnmpt  15016  txdis1cn  15021  cnmptcom  15041  imasnopn  15042  hmeocnv  15050  hmeores  15058  txhmeo  15062  txswaphmeo  15064  ispsmet  15066  xmetres  15125  metres  15126  blex  15130  xmeter  15179  xmetresbl  15183  mopntopon  15186  isxms2  15195  xmetxp  15250  xmettx  15253  txmetcnp  15261  qtopbasss  15264  qtopbas  15265  reopnap  15289  ioo2blex  15295  blssioo  15296  tgioo  15297  fsumcncntop  15310  expcn  15312  cncfval  15315  divccncfap  15333  cdivcncfap  15347  divcncfap  15357  maxcncf  15358  mincncf  15359  ivthdec  15387  hoverb  15391  limccnpcntop  15418  dvrecap  15456  elplyd  15484  ply1termlem  15485  ply1term  15486  plymullem1  15491  plyaddlem  15492  plymullem  15493  plycolemc  15501  plyco  15502  plycj  15504  plycn  15505  plyreres  15507  dvply1  15508  dvply2g  15509  pilem3  15526  tanrpcl  15580  cosordlem  15592  ioocosf1o  15597  rpcncxpcl  15645  rpcxpcl  15646  rpabscxpbnd  15683  rplogbcl  15689  sgmnncl  15731  mpodvdsmulf1o  15733  fsumdvdsmul  15734  mersenne  15740  perfectlem2  15743  lgslem1  15748  lgsval  15752  lgscllem  15755  lgsne0  15786  gausslemma2dlem4  15812  lgseisenlem1  15818  lgsquadlem1  15825  lgsquadlem2  15826  2sqlem3  15865  2sqlem8  15871  vtxex  15888  iedgex  15889  edgvalg  15929  edgopval  15932  edgstruct  15934  usgrausgrien  16039  ausgrumgrien  16040  ausgrusgrien  16041  uspgr1ewopdc  16114  usgr2v1e2w  16116  uhgrspansubgrlem  16146  vtxdgfif  16163  vtxdfifiun  16167  1loopgrvd2fi  16175  1loopgrvd0fi  16176  1hevtxdg0fi  16177  1hevtxdg1en  16178  p1evtxdeqfilem  16181  vdegp1bid  16185  wlkex  16195  wlkelvv  16219  clwwlkccat  16271  clwwlknonex2lem1  16307  clwwlknonex2lem2  16308  clwwlknonex2  16309  trlsegvdeglem6  16335  trlsegvdeglem7  16336  trlsegvdegfi  16337  eupth2lem3lem1fi  16338  eupth2lem3lem2fi  16339  eupth2lem3lem5  16342  eupth2lembfi  16347  eulerpathprum  16350  depindlem1  16376  depindlem2  16377  djucllem  16447  012of  16643  2o01f  16644  nninfsellemeq  16667  qdencn  16682  cvgcmp2nlemabs  16687  trilpolemclim  16691  trilpolemisumle  16693  trilpolemeq1  16695  trilpolemlt1  16696  nconstwlpolemgt0  16720  gfsumval  16732  gfsumsn  16737  gfsumcl  16739