Theorem eqeltri 2304

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

Syntax hints:   = 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:  eqeltrri  2305  3eltr4i  2313  intab  3957  inex2  4224  vpwex  4269  ord3ex  4280  uniopel  4349  onsucelsucexmid  4628  nnpredcl  4721  elvvuni  4790  isarep2  5417  acexmidlemcase  6013  abrexex2  6286  oprabex  6290  oprabrexex2  6292  mpoexw  6378  rdg0  6553  frecex  6560  1on  6589  2on  6591  3on  6593  4on  6595  2oex  6599  1onn  6688  2onn  6689  3onn  6690  4onn  6691  mapsnf1o2  6865  exmidpw  7100  exmidpw2en  7104  unfiexmid  7110  xpfi  7124  ssfirab  7129  fnfi  7135  iunfidisj  7145  fidcenumlemr  7154  sbthlemi10  7165  ctmlemr  7307  nninfex  7320  exmidonfinlem  7404  acfun  7422  exmidaclem  7423  pw1ne1  7447  ccfunen  7483  nqex  7583  nq0ex  7660  1pr  7774  ltexprlempr  7828  recexprlempr  7852  cauappcvgprlemcl  7873  caucvgprlemcl  7896  caucvgprprlemcl  7924  addvalex  8064  peano1nnnn  8072  peano2nnnn  8073  axcnex  8079  ax1cn  8081  ax1re  8082  pnfxr  8232  mnfxr  8236  inelr  8764  cju  9141  2re  9213  3re  9217  4re  9220  5re  9222  6re  9224  7re  9226  8re  9228  9re  9230  2nn  9305  3nn  9306  4nn  9307  5nn  9308  6nn  9309  7nn  9310  8nn  9311  9nn  9312  nn0ex  9408  nneoor  9582  zeo  9585  deccl  9625  decnncl  9630  numnncl2  9633  decnncl2  9634  numsucc  9650  numma2c  9656  numadd  9657  numaddc  9658  nummul1c  9659  nummul2c  9660  xnegcl  10067  xrex  10091  ioof  10206  uzennn  10699  xnn0nnen  10700  seqex  10712  m1expcl2  10824  faccl  10998  facwordi  11003  faclbnd2  11005  bccl  11030  lswex  11169  crre  11422  remim  11425  absval  11566  climle  11899  climcvg1nlem  11914  iserabs  12041  geo2lim  12082  prodfclim1  12110  fprodle  12206  ere  12236  ege2le3  12237  eftlub  12256  efsep  12257  tan0  12297  ef01bndlem  12322  nn0o  12473  pczpre  12875  pockthi  12936  igz  12952  ennnfonelemj0  13027  ennnfonelem0  13031  ndxarg  13110  ndxslid  13112  strndxid  13115  basendxnn  13143  strle1g  13194  plusgndxnn  13199  2strbasg  13208  2stropg  13209  tsetndxnn  13277  plendxnn  13291  dsndxnn  13306  unifndxnn  13316  rmodislmodlem  14370  rmodislmod  14371  cndsex  14573  znval  14656  znle  14657  znbaslemnn  14659  znbas  14664  znzrhval  14667  psrval  14686  fczpsrbag  14691  setsmsbasg  15209  cnbl0  15264  cnopncntop  15274  cnopn  15275  remet  15278  divcnap  15295  expcn  15299  climcncf  15314  idcncf  15331  expcncf  15339  cnrehmeocntop  15340  hovercncf  15376  plyrecj  15493  sincn  15499  coscn  15500  2logb9irrALT  15704  2irrexpq  15706  2irrexpqap  15708  lgslem4  15738  lgsdir2lem2  15764  edgfndxnn  15865  setsvtx  15908  usgrstrrepeen  16088  eulerpathprum  16337  bdinex2  16521  bj-inex  16528  012of  16618  2o01f  16619  peano3nninf  16635  cvgcmp2nlemabs  16662  trilpolemisumle  16668