Theorem eqeltri 2266

Description: Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
eqeltr.1	⊢ 𝐴 = 𝐵
eqeltr.2	⊢ 𝐵 ∈ 𝐶

Assertion

Ref	Expression
eqeltri	⊢ 𝐴 ∈ 𝐶

Proof of Theorem eqeltri

Step	Hyp	Ref	Expression
1		eqeltr.2	. 2 ⊢ 𝐵 ∈ 𝐶
2		eqeltr.1	. . 3 ⊢ 𝐴 = 𝐵
3	2	eleq1i 2259	. 2 ⊢ (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶)
4	1, 3	mpbir 146	1 ⊢ 𝐴 ∈ 𝐶

Syntax hints:   = wceq 1364   ∈ wcel 2164

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-cleq 2186  df-clel 2189

This theorem is referenced by:  eqeltrri  2267  3eltr4i  2275  intab  3899  inex2  4164  vpwex  4208  ord3ex  4219  uniopel  4285  onsucelsucexmid  4562  nnpredcl  4655  elvvuni  4723  isarep2  5341  acexmidlemcase  5913  abrexex2  6176  oprabex  6180  oprabrexex2  6182  mpoexw  6266  rdg0  6440  frecex  6447  1on  6476  2on  6478  3on  6480  4on  6481  1onn  6573  2onn  6574  3onn  6575  4onn  6576  mapsnf1o2  6750  exmidpw  6964  exmidpw2en  6968  unfiexmid  6974  xpfi  6986  ssfirab  6990  fnfi  6995  iunfidisj  7005  fidcenumlemr  7014  sbthlemi10  7025  ctmlemr  7167  nninfex  7180  exmidonfinlem  7253  acfun  7267  exmidaclem  7268  pw1ne1  7289  ccfunen  7324  nqex  7423  nq0ex  7500  1pr  7614  ltexprlempr  7668  recexprlempr  7692  cauappcvgprlemcl  7713  caucvgprlemcl  7736  caucvgprprlemcl  7764  addvalex  7904  peano1nnnn  7912  peano2nnnn  7913  axcnex  7919  ax1cn  7921  ax1re  7922  pnfxr  8072  mnfxr  8076  inelr  8603  cju  8980  2re  9052  3re  9056  4re  9059  5re  9061  6re  9063  7re  9065  8re  9067  9re  9069  2nn  9143  3nn  9144  4nn  9145  5nn  9146  6nn  9147  7nn  9148  8nn  9149  9nn  9150  nn0ex  9246  nneoor  9419  zeo  9422  deccl  9462  decnncl  9467  numnncl2  9470  decnncl2  9471  numsucc  9487  numma2c  9493  numadd  9494  numaddc  9495  nummul1c  9496  nummul2c  9497  xnegcl  9898  xrex  9922  ioof  10037  uzennn  10507  xnn0nnen  10508  seqex  10520  m1expcl2  10632  faccl  10806  facwordi  10811  faclbnd2  10813  bccl  10838  crre  11001  remim  11004  absval  11145  climle  11477  climcvg1nlem  11492  iserabs  11618  geo2lim  11659  prodfclim1  11687  fprodle  11783  ere  11813  ege2le3  11814  eftlub  11833  efsep  11834  tan0  11874  ef01bndlem  11899  nn0o  12048  pczpre  12435  pockthi  12496  igz  12512  ennnfonelemj0  12558  ennnfonelem0  12562  ndxarg  12641  ndxslid  12643  strndxid  12646  basendxnn  12674  strle1g  12724  plusgndxnn  12729  2strbasg  12737  2stropg  12738  tsetndxnn  12806  plendxnn  12820  dsndxnn  12831  unifndxnn  12841  rmodislmodlem  13846  rmodislmod  13847  znval  14124  znle  14125  znbaslemnn  14127  znbas  14132  znzrhval  14135  psrval  14152  fczpsrbag  14157  setsmsbasg  14647  cnbl0  14702  cnopncntop  14705  remet  14708  divcnap  14723  climcncf  14739  idcncf  14755  expcncf  14763  cnrehmeocntop  14764  hovercncf  14800  sincn  14904  coscn  14905  2logb9irrALT  15106  2irrexpq  15108  2irrexpqap  15110  lgslem4  15119  lgsdir2lem2  15145  bdinex2  15392  bj-inex  15399  012of  15486  2o01f  15487  peano3nninf  15497  cvgcmp2nlemabs  15522  trilpolemisumle  15528