Theorem eqeltrd 2217

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

Syntax hints:   → wi 4   = wceq 1332   ∈ wcel 1481

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 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515  ax-ext 2122

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

This theorem is referenced by:  eqeltrrd  2218  3eltr4d  2224  eqeltrid  2227  eqeltrdi  2231  ifcldadc  3506  ifcldcd  3512  intab  3808  disjiun  3932  iinexgm  4087  opexg  4158  tfisi  4509  nnpredcl  4544  imain  5213  fvmptd  5510  fvmptdf  5516  fvmptt  5520  elfvmptrab  5524  dffo3  5575  resfunexg  5649  f1oiso2  5736  riota2df  5758  riota5f  5762  ovmpodxf  5904  ovmpodf  5910  offval  5997  ofvalg  5999  offeq  6003  iunexg  6025  oprabexd  6033  fo1stresm  6067  fo2ndresm  6068  oprssdmm  6077  1stdm  6088  1stconst  6126  2ndconst  6127  cnvf1olem  6129  fo2ndf  6132  f1od2  6140  iunon  6189  tfrlemibacc  6231  tfrlemibfn  6233  tfr1onlembacc  6247  tfr1onlembfn  6249  tfrcllembacc  6260  tfrcllembfn  6262  tfrcl  6269  rdgon  6291  frec0g  6302  freccllem  6307  frecfcllem  6309  frecsuclem  6311  oacl  6364  omcl  6365  oeicl  6366  nntr2  6407  mptelixpg  6636  fidifsnen  6772  en2eqpr  6809  unfiin  6822  ssfirab  6830  fnfi  6833  relcnvfi  6837  fidcenumlemr  6851  elfi2  6868  supclti  6893  supubti  6894  suplubti  6895  supelti  6897  ordiso2  6928  djulclr  6942  djurclr  6943  djulcl  6944  djurcl  6945  djuss  6963  updjudhcoinlf  6973  updjudhcoinrg  6974  ctssdclemn0  7003  ctssdccl  7004  ctssdc  7006  enumctlemm  7007  cardcl  7054  cc2lem  7098  cc3  7100  addclpi  7159  mulclpi  7160  addclnq  7207  mulclnq  7208  addclnq0  7283  mulclnq0  7284  nqpnq0nq  7285  elnp1st2nd  7308  prarloclemcalc  7334  distrlem1prl  7414  distrlem1pru  7415  ltexprlemopl  7433  ltexprlemopu  7435  ltexprlemfl  7441  ltexprlemrl  7442  ltexprlemfu  7443  ltexprlemru  7444  addcanprlemu  7447  recexprlemloc  7463  aptiprleml  7471  caucvgprprlemopl  7529  suplocexprlemex  7554  addclsr  7585  mulclsr  7586  recexgt0sr  7605  mulextsr1lem  7612  suplocsrlemb  7638  suplocsrlempr  7639  suplocsrlem  7640  axaddcl  7696  axaddrcl  7697  axmulcl  7698  axmulrcl  7699  axcaucvglemval  7729  subcl  7985  cru  8388  aprcl  8432  divclap  8462  redivclap  8515  diveqap1bd  8619  lbinfcl  8731  cju  8743  nn1m1nn  8762  nnsub  8783  nnnn0addcl  9031  un0addcl  9034  peano2z  9114  peano2zm  9116  zaddcllemneg  9117  zaddcl  9118  nnaddm1cl  9139  nn0n0n1ge2  9145  zdivadd  9164  zdivmul  9165  suprzclex  9173  zneo  9176  peano5uzti  9183  supinfneg  9417  infsupneg  9418  qmulz  9442  qnegcl  9455  qapne  9458  qdivcl  9462  cnref1o  9469  xnegcl  9645  xltnegi  9648  xaddnemnf  9670  xaddnepnf  9671  xnegdi  9681  xnpcan  9685  xltadd1  9689  xposdif  9695  xleaddadd  9700  iccf1o  9817  ige3m2fz  9860  ige2m1fz1  9920  rebtwn2z  10063  flqcl  10077  flapcl  10079  ceilqcl  10112  intfracq  10124  modqcl  10130  mulqmod0  10134  modqdifz  10140  zmodcl  10148  modfzo0difsn  10199  modsumfzodifsn  10200  frec2uzzd  10204  frec2uzsucd  10205  frec2uzuzd  10206  frecuzrdgrrn  10212  frec2uzrdg  10213  frecuzrdgrcl  10214  frecuzrdgsuc  10218  frecuzrdgrclt  10219  frecuzrdgg  10220  frecuzrdgsuctlem  10227  fzofig  10236  iseqovex  10260  seq3val  10262  seqvalcd  10263  seqf  10265  seqovcd  10267  seq3clss  10271  seq3caopr3  10285  iseqf1olemnab  10292  iseqf1olemqk  10298  iseqf1olemjpcl  10299  iseqf1olemqpcl  10300  iseqf1olemfvp  10301  seq3f1olemqsumkj  10302  seq3f1olemqsum  10304  seq3f1oleml  10307  seq3f1o  10308  seq3distr  10317  ser0f  10319  ser3le  10322  exp3vallem  10325  exp3val  10326  exp1  10330  expcl2lemap  10336  m1expcl2  10346  expaddzap  10368  sqcl  10385  nnsqcl  10393  qsqcl  10395  zesq  10441  facp1  10508  faccl  10513  facdiv  10516  bcval  10527  bcrpcl  10531  bcp1n  10539  bcpasc  10544  permnn  10549  hashennn  10558  hashcl  10559  shftlem  10620  ovshftex  10623  shftf  10634  seq3shft  10642  cjth  10650  imval  10654  recl  10657  imcl  10658  crre  10661  remim  10664  reim0b  10666  cvg1nlemcau  10788  uzin2  10791  resqrexlem1arp  10809  resqrexlemp1rp  10810  resqrexlemglsq  10826  resqrexlemga  10827  resqrtcl  10833  abscl  10855  absrpclap  10865  nn0abscl  10889  fzomaxdiflem  10916  fzomaxdif  10917  maxabslemab  11010  maxcl  11014  zmaxcl  11028  minmax  11033  mincl  11034  xrmaxcl  11053  xrmaxaddlem  11061  xrminmax  11066  xrmincl  11067  xrmineqinf  11070  xrminrpcl  11075  reccn2ap  11114  climaddc1  11130  climmulc2  11132  climsubc1  11133  climsubc2  11134  climle  11135  climlec2  11142  climcvg1nlem  11150  sumrbdclem  11178  fsum3cvg  11179  summodclem3  11181  summodclem2a  11182  zsumdc  11185  fsumgcl  11187  fsum3  11188  isumss  11192  fisumss  11193  isumss2  11194  fsum3cvg2  11195  fsum3ser  11198  fsumcl2lem  11199  fsumcllem  11200  fsumadd  11207  sumsnf  11210  fsumsplitsn  11211  isumcl  11226  isummulc2  11227  isumrecl  11230  isumge0  11231  isumadd  11232  fsum2dlemstep  11235  fisumcom2  11239  mptfzshft  11243  fsumrev  11244  fsummulc2  11249  iserabs  11276  isumshft  11291  isumsplit  11292  isum1p  11293  isumrpcl  11295  isumle  11296  isumlessdc  11297  trireciplem  11301  expcnvap0  11303  expcnvre  11304  expcnv  11305  explecnv  11306  geolim  11312  geolim2  11313  geo2lim  11317  cvgratnnlemsumlt  11329  cvgratz  11333  mertenslemub  11335  mertenslemi1  11336  mertenslem2  11337  mertensabs  11338  prodf1f  11344  prodfdivap  11348  prodrbdclem  11372  fproddccvg  11373  prodmodclem3  11376  prodmodclem2a  11377  zproddc  11380  fprodseq  11384  efcllemp  11401  ef0lem  11403  efcvgfsum  11410  reefcl  11411  ege2le3  11414  efcj  11416  efaddlem  11417  eftlcvg  11430  eftlcl  11431  reeftlcl  11432  eftlub  11433  efsep  11434  effsumlt  11435  efgt1p2  11438  efgt1p  11439  reeff1  11443  tanclap  11452  resincl  11463  recoscl  11464  retanclap  11465  eirraplem  11519  dvdsval2  11532  sqoddm1div8z  11619  zssinfcl  11677  infssuzex  11678  infssuzcldc  11680  gcdval  11684  gcdn0cl  11687  gcddvds  11688  divgcdnnr  11700  nn0seqcvgd  11758  ialgrlem1st  11759  ialgrlemconst  11760  algrf  11762  algrp1  11763  eucalgf  11772  eucalglt  11774  lcmval  11780  lcmcllem  11784  lcmgcdlem  11794  cncongr2  11821  sqrt2irrlem  11875  oddpwdclemxy  11883  oddpwdclemdc  11887  qden1elz  11919  phicl2  11926  phimullem  11937  ennnfonelemjn  11951  ennnfonelemg  11952  ennnfonelemp1  11955  ctinfomlemom  11976  ctiunctlemfo  11988  setsex  12030  strsetsid  12031  ressid2  12057  ressval2  12058  ressid  12059  iunopn  12208  toponmax  12231  tgvalex  12258  tgtop  12276  tgiun  12281  tgidm  12282  ntropn  12325  tgrest  12377  restopnb  12389  cnovex  12404  cnclima  12431  txvalex  12462  txtop  12468  tx1cn  12477  tx2cn  12478  txcnp  12479  txcnmpt  12481  txdis1cn  12486  cnmptcom  12506  imasnopn  12507  hmeocnv  12515  hmeores  12523  txhmeo  12527  txswaphmeo  12529  ispsmet  12531  xmetres  12590  metres  12591  blex  12595  xmeter  12644  xmetresbl  12648  mopntopon  12651  isxms2  12660  xmetxp  12715  xmettx  12718  txmetcnp  12726  qtopbasss  12729  qtopbas  12730  reopnap  12746  ioo2blex  12752  blssioo  12753  tgioo  12754  fsumcncntop  12764  cncfval  12767  divccncfap  12785  cdivcncfap  12795  ivthdec  12830  limccnpcntop  12852  dvrecap  12885  pilem3  12912  tanrpcl  12966  cosordlem  12978  ioocosf1o  12983  rpcncxpcl  13031  rpcxpcl  13032  rpabscxpbnd  13067  rplogbcl  13071  djucllem  13178  012of  13363  2o01f  13364  nninfsellemeq  13385  qdencn  13397  cvgcmp2nlemabs  13402  trilpolemclim  13404  trilpolemisumle  13406  trilpolemeq1  13408  trilpolemlt1  13409