Theorem eqeltri 2305

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

Syntax hints:   = wceq 1398   ∈ wcel 2203

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-cleq 2225  df-clel 2228

This theorem is referenced by:  eqeltrri  2306  3eltr4i  2314  intab  3978  inex2  4245  vpwex  4292  ord3ex  4303  vsnex  4324  uniopel  4373  onsucelsucexmid  4652  nnpredcl  4745  elvvuni  4814  isarep2  5443  acexmidlemcase  6045  abrexex2  6317  oprabex  6321  oprabrexex2  6323  mpoexw  6409  rdg0  6618  frecex  6625  1on  6654  2on  6656  3on  6658  4on  6660  2oex  6664  1onn  6753  2onn  6754  3onn  6755  4onn  6756  mapsnf1o2  6931  exmidpw  7168  exmidpw2en  7172  unfiexmid  7178  xpfi  7192  ssfirab  7197  fnfi  7203  iunfidisj  7213  fidcenumlemr  7225  sbthlemi10  7236  fczfsuppd  7250  ctmlemr  7399  nninfex  7412  exmidonfinlem  7496  acfun  7514  exmidaclem  7515  pw1ne1  7539  ccfunen  7578  nqex  7678  nq0ex  7755  1pr  7869  ltexprlempr  7923  recexprlempr  7947  cauappcvgprlemcl  7968  caucvgprlemcl  7991  caucvgprprlemcl  8019  addvalex  8159  peano1nnnn  8167  peano2nnnn  8168  axcnex  8174  ax1cn  8176  ax1re  8177  pnfxr  8326  mnfxr  8330  inelr  8858  cju  9235  2re  9307  3re  9311  4re  9314  5re  9316  6re  9318  7re  9320  8re  9322  9re  9324  2nn  9399  3nn  9400  4nn  9401  5nn  9402  6nn  9403  7nn  9404  8nn  9405  9nn  9406  nn0ex  9502  nneoor  9680  zeo  9683  deccl  9723  decnncl  9728  numnncl2  9731  decnncl2  9732  numsucc  9748  numma2c  9754  numadd  9755  numaddc  9756  nummul1c  9757  nummul2c  9758  xnegcl  10165  xrex  10189  ioof  10304  uzennn  10798  xnn0nnen  10799  seqex  10811  m1expcl2  10923  faccl  11097  facwordi  11102  faclbnd2  11104  bccl  11129  lswex  11276  crre  11542  remim  11545  absval  11686  climle  12019  climcvg1nlem  12034  iserabs  12161  geo2lim  12202  prodfclim1  12230  fprodle  12326  ere  12356  ege2le3  12357  eftlub  12376  efsep  12377  tan0  12417  ef01bndlem  12442  nn0o  12593  pczpre  12995  pockthi  13056  igz  13072  ballotfilemofi  13138  ballotfilemonn  13140  ennnfonelemj0  13152  ennnfonelem0  13156  ndxarg  13235  ndxslid  13237  strndxid  13240  basendxnn  13268  strle1g  13319  plusgndxnn  13324  2strbasg  13333  2stropg  13334  tsetndxnn  13402  plendxnn  13416  dsndxnn  13431  unifndxnn  13441  rmodislmodlem  14498  rmodislmod  14499  cndsex  14701  znval  14784  znle  14785  znbaslemnn  14787  znbas  14792  znzrhval  14795  psrval  14814  fczpsrbag  14820  setsmsbasg  15344  cnbl0  15399  cnopncntop  15409  cnopn  15410  remet  15413  divcnap  15430  expcn  15434  climcncf  15449  idcncf  15466  expcncf  15474  cnrehmeocntop  15475  hovercncf  15511  plyrecj  15628  sincn  15634  coscn  15635  2logb9irrALT  15839  2irrexpq  15841  2irrexpqap  15843  lgslem4  15876  lgsdir2lem2  15902  edgfndxnn  16003  setsvtx  16046  usgrstrrepeen  16226  eulerpathprum  16475  konigsbergumgr  16482  konigsberglem5  16487  konigsberg  16488  bdinex2  16670  bj-inex  16677  012of  16767  2o01f  16768  peano3nninf  16785  cvgcmp2nlemabs  16816  trilpolemisumle  16822