Theorem eqeltrd 2214

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

Syntax hints:   → wi 4   = wceq 1331   ∈ wcel 1480

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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-cleq 2130  df-clel 2133

This theorem is referenced by:  eqeltrrd  2215  3eltr4d  2221  eqeltrid  2224  eqeltrdi  2228  ifcldadc  3496  ifcldcd  3502  intab  3795  disjiun  3919  iinexgm  4074  opexg  4145  tfisi  4496  nnpredcl  4531  imain  5200  fvmptd  5495  fvmptdf  5501  fvmptt  5505  elfvmptrab  5509  dffo3  5560  resfunexg  5634  f1oiso2  5721  riota2df  5743  riota5f  5747  ovmpodxf  5889  ovmpodf  5895  offval  5982  ofvalg  5984  offeq  5988  iunexg  6010  oprabexd  6018  fo1stresm  6052  fo2ndresm  6053  oprssdmm  6062  1stdm  6073  1stconst  6111  2ndconst  6112  cnvf1olem  6114  fo2ndf  6117  f1od2  6125  iunon  6174  tfrlemibacc  6216  tfrlemibfn  6218  tfr1onlembacc  6232  tfr1onlembfn  6234  tfrcllembacc  6245  tfrcllembfn  6247  tfrcl  6254  rdgon  6276  frec0g  6287  freccllem  6292  frecfcllem  6294  frecsuclem  6296  oacl  6349  omcl  6350  oeicl  6351  nntr2  6392  mptelixpg  6621  fidifsnen  6757  en2eqpr  6794  unfiin  6807  ssfirab  6815  fnfi  6818  relcnvfi  6822  fidcenumlemr  6836  elfi2  6853  supclti  6878  supubti  6879  suplubti  6880  supelti  6882  ordiso2  6913  djulclr  6927  djurclr  6928  djulcl  6929  djurcl  6930  djuss  6948  updjudhcoinlf  6958  updjudhcoinrg  6959  ctssdclemn0  6988  ctssdccl  6989  ctssdc  6991  enumctlemm  6992  cardcl  7030  addclpi  7128  mulclpi  7129  addclnq  7176  mulclnq  7177  addclnq0  7252  mulclnq0  7253  nqpnq0nq  7254  elnp1st2nd  7277  prarloclemcalc  7303  distrlem1prl  7383  distrlem1pru  7384  ltexprlemopl  7402  ltexprlemopu  7404  ltexprlemfl  7410  ltexprlemrl  7411  ltexprlemfu  7412  ltexprlemru  7413  addcanprlemu  7416  recexprlemloc  7432  aptiprleml  7440  caucvgprprlemopl  7498  suplocexprlemex  7523  addclsr  7554  mulclsr  7555  recexgt0sr  7574  mulextsr1lem  7581  suplocsrlemb  7607  suplocsrlempr  7608  suplocsrlem  7609  axaddcl  7665  axaddrcl  7666  axmulcl  7667  axmulrcl  7668  axcaucvglemval  7698  subcl  7954  cru  8357  aprcl  8401  divclap  8431  redivclap  8484  diveqap1bd  8588  lbinfcl  8700  cju  8712  nn1m1nn  8731  nnsub  8752  nnnn0addcl  9000  un0addcl  9003  peano2z  9083  peano2zm  9085  zaddcllemneg  9086  zaddcl  9087  nnaddm1cl  9108  nn0n0n1ge2  9114  zdivadd  9133  zdivmul  9134  suprzclex  9142  zneo  9145  peano5uzti  9152  supinfneg  9383  infsupneg  9384  qmulz  9408  qnegcl  9421  qapne  9424  qdivcl  9428  cnref1o  9433  xnegcl  9608  xltnegi  9611  xaddnemnf  9633  xaddnepnf  9634  xnegdi  9644  xnpcan  9648  xltadd1  9652  xposdif  9658  xleaddadd  9663  iccf1o  9780  ige3m2fz  9822  ige2m1fz1  9882  rebtwn2z  10025  flqcl  10039  flapcl  10041  ceilqcl  10074  intfracq  10086  modqcl  10092  mulqmod0  10096  modqdifz  10102  zmodcl  10110  modfzo0difsn  10161  modsumfzodifsn  10162  frec2uzzd  10166  frec2uzsucd  10167  frec2uzuzd  10168  frecuzrdgrrn  10174  frec2uzrdg  10175  frecuzrdgrcl  10176  frecuzrdgsuc  10180  frecuzrdgrclt  10181  frecuzrdgg  10182  frecuzrdgsuctlem  10189  fzofig  10198  iseqovex  10222  seq3val  10224  seqvalcd  10225  seqf  10227  seqovcd  10229  seq3clss  10233  seq3caopr3  10247  iseqf1olemnab  10254  iseqf1olemqk  10260  iseqf1olemjpcl  10261  iseqf1olemqpcl  10262  iseqf1olemfvp  10263  seq3f1olemqsumkj  10264  seq3f1olemqsum  10266  seq3f1oleml  10269  seq3f1o  10270  seq3distr  10279  ser0f  10281  ser3le  10284  exp3vallem  10287  exp3val  10288  exp1  10292  expcl2lemap  10298  m1expcl2  10308  expaddzap  10330  sqcl  10347  nnsqcl  10355  qsqcl  10357  zesq  10403  facp1  10469  faccl  10474  facdiv  10477  bcval  10488  bcrpcl  10492  bcp1n  10500  bcpasc  10505  permnn  10510  hashennn  10519  hashcl  10520  shftlem  10581  ovshftex  10584  shftf  10595  seq3shft  10603  cjth  10611  imval  10615  recl  10618  imcl  10619  crre  10622  remim  10625  reim0b  10627  cvg1nlemcau  10749  uzin2  10752  resqrexlem1arp  10770  resqrexlemp1rp  10771  resqrexlemglsq  10787  resqrexlemga  10788  resqrtcl  10794  abscl  10816  absrpclap  10826  nn0abscl  10850  fzomaxdiflem  10877  fzomaxdif  10878  maxabslemab  10971  maxcl  10975  zmaxcl  10989  minmax  10994  mincl  10995  xrmaxcl  11014  xrmaxaddlem  11022  xrminmax  11027  xrmincl  11028  xrmineqinf  11031  xrminrpcl  11036  reccn2ap  11075  climaddc1  11091  climmulc2  11093  climsubc1  11094  climsubc2  11095  climle  11096  climlec2  11103  climcvg1nlem  11111  sumrbdclem  11138  fsum3cvg  11139  summodclem3  11142  summodclem2a  11143  zsumdc  11146  fsumgcl  11148  fsum3  11149  isumss  11153  fisumss  11154  isumss2  11155  fsum3cvg2  11156  fsum3ser  11159  fsumcl2lem  11160  fsumcllem  11161  fsumadd  11168  sumsnf  11171  fsumsplitsn  11172  isumcl  11187  isummulc2  11188  isumrecl  11191  isumge0  11192  isumadd  11193  fsum2dlemstep  11196  fisumcom2  11200  mptfzshft  11204  fsumrev  11205  fsummulc2  11210  iserabs  11237  isumshft  11252  isumsplit  11253  isum1p  11254  isumrpcl  11256  isumle  11257  isumlessdc  11258  trireciplem  11262  expcnvap0  11264  expcnvre  11265  expcnv  11266  explecnv  11267  geolim  11273  geolim2  11274  geo2lim  11278  cvgratnnlemsumlt  11290  cvgratz  11294  mertenslemub  11296  mertenslemi1  11297  mertenslem2  11298  mertensabs  11299  prodf1f  11305  prodfdivap  11309  prodrbdclem  11333  fproddccvg  11334  efcllemp  11353  ef0lem  11355  efcvgfsum  11362  reefcl  11363  ege2le3  11366  efcj  11368  efaddlem  11369  eftlcvg  11382  eftlcl  11383  reeftlcl  11384  eftlub  11385  efsep  11386  effsumlt  11387  efgt1p2  11390  efgt1p  11391  reeff1  11396  tanclap  11405  resincl  11416  recoscl  11417  retanclap  11418  eirraplem  11472  dvdsval2  11485  sqoddm1div8z  11572  zssinfcl  11630  infssuzex  11631  infssuzcldc  11633  gcdval  11637  gcdn0cl  11640  gcddvds  11641  divgcdnnr  11653  nn0seqcvgd  11711  ialgrlem1st  11712  ialgrlemconst  11713  algrf  11715  algrp1  11716  eucalgf  11725  eucalglt  11727  lcmval  11733  lcmcllem  11737  lcmgcdlem  11747  cncongr2  11774  sqrt2irrlem  11828  oddpwdclemxy  11836  oddpwdclemdc  11840  qden1elz  11872  phicl2  11879  phimullem  11890  ennnfonelemjn  11904  ennnfonelemg  11905  ennnfonelemp1  11908  ctinfomlemom  11929  ctiunctlemfo  11941  setsex  11980  strsetsid  11981  ressid2  12007  ressval2  12008  ressid  12009  iunopn  12158  toponmax  12181  tgvalex  12208  tgtop  12226  tgiun  12231  tgidm  12232  ntropn  12275  tgrest  12327  restopnb  12339  cnovex  12354  cnclima  12381  txvalex  12412  txtop  12418  tx1cn  12427  tx2cn  12428  txcnp  12429  txcnmpt  12431  txdis1cn  12436  cnmptcom  12456  imasnopn  12457  hmeocnv  12465  hmeores  12473  txhmeo  12477  txswaphmeo  12479  ispsmet  12481  xmetres  12540  metres  12541  blex  12545  xmeter  12594  xmetresbl  12598  mopntopon  12601  isxms2  12610  xmetxp  12665  xmettx  12668  txmetcnp  12676  qtopbasss  12679  qtopbas  12680  reopnap  12696  ioo2blex  12702  blssioo  12703  tgioo  12704  fsumcncntop  12714  cncfval  12717  divccncfap  12735  cdivcncfap  12745  ivthdec  12780  limccnpcntop  12802  dvrecap  12835  pilem3  12853  tanrpcl  12907  cosordlem  12919  djucllem  12996  nninfsellemeq  13199  qdencn  13211  isomninnlem  13214  cvgcmp2nlemabs  13216  trilpolemclim  13218  trilpolemisumle  13220  trilpolemeq1  13222  trilpolemlt1  13223