Theorem eqeltri 2277

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 2270	. 2 ⊢ (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶)
4	1, 3	mpbir 146	1 ⊢ 𝐴 ∈ 𝐶

Syntax hints:   = wceq 1372   ∈ wcel 2175

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 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532  ax-17 1548  ax-ial 1556  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-cleq 2197  df-clel 2200

This theorem is referenced by:  eqeltrri  2278  3eltr4i  2286  intab  3913  inex2  4178  vpwex  4222  ord3ex  4233  uniopel  4300  onsucelsucexmid  4577  nnpredcl  4670  elvvuni  4738  isarep2  5360  acexmidlemcase  5938  abrexex2  6208  oprabex  6212  oprabrexex2  6214  mpoexw  6298  rdg0  6472  frecex  6479  1on  6508  2on  6510  3on  6512  4on  6513  1onn  6605  2onn  6606  3onn  6607  4onn  6608  mapsnf1o2  6782  exmidpw  7004  exmidpw2en  7008  unfiexmid  7014  xpfi  7028  ssfirab  7032  fnfi  7037  iunfidisj  7047  fidcenumlemr  7056  sbthlemi10  7067  ctmlemr  7209  nninfex  7222  exmidonfinlem  7300  acfun  7318  exmidaclem  7319  pw1ne1  7340  ccfunen  7375  nqex  7475  nq0ex  7552  1pr  7666  ltexprlempr  7720  recexprlempr  7744  cauappcvgprlemcl  7765  caucvgprlemcl  7788  caucvgprprlemcl  7816  addvalex  7956  peano1nnnn  7964  peano2nnnn  7965  axcnex  7971  ax1cn  7973  ax1re  7974  pnfxr  8124  mnfxr  8128  inelr  8656  cju  9033  2re  9105  3re  9109  4re  9112  5re  9114  6re  9116  7re  9118  8re  9120  9re  9122  2nn  9197  3nn  9198  4nn  9199  5nn  9200  6nn  9201  7nn  9202  8nn  9203  9nn  9204  nn0ex  9300  nneoor  9474  zeo  9477  deccl  9517  decnncl  9522  numnncl2  9525  decnncl2  9526  numsucc  9542  numma2c  9548  numadd  9549  numaddc  9550  nummul1c  9551  nummul2c  9552  xnegcl  9953  xrex  9977  ioof  10092  uzennn  10579  xnn0nnen  10580  seqex  10592  m1expcl2  10704  faccl  10878  facwordi  10883  faclbnd2  10885  bccl  10910  crre  11110  remim  11113  absval  11254  climle  11587  climcvg1nlem  11602  iserabs  11728  geo2lim  11769  prodfclim1  11797  fprodle  11893  ere  11923  ege2le3  11924  eftlub  11943  efsep  11944  tan0  11984  ef01bndlem  12009  nn0o  12160  pczpre  12562  pockthi  12623  igz  12639  ennnfonelemj0  12714  ennnfonelem0  12718  ndxarg  12797  ndxslid  12799  strndxid  12802  basendxnn  12830  strle1g  12880  plusgndxnn  12885  2strbasg  12894  2stropg  12895  tsetndxnn  12963  plendxnn  12977  dsndxnn  12992  unifndxnn  13002  rmodislmodlem  14054  rmodislmod  14055  cndsex  14257  znval  14340  znle  14341  znbaslemnn  14343  znbas  14348  znzrhval  14351  psrval  14370  fczpsrbag  14375  setsmsbasg  14893  cnbl0  14948  cnopncntop  14958  cnopn  14959  remet  14962  divcnap  14979  expcn  14983  climcncf  14998  idcncf  15015  expcncf  15023  cnrehmeocntop  15024  hovercncf  15060  plyrecj  15177  sincn  15183  coscn  15184  2logb9irrALT  15388  2irrexpq  15390  2irrexpqap  15392  lgslem4  15422  lgsdir2lem2  15448  edgfndxnn  15549  bdinex2  15769  bj-inex  15776  012of  15863  2o01f  15864  peano3nninf  15877  cvgcmp2nlemabs  15904  trilpolemisumle  15910