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  6012  abrexex2  6285  oprabex  6289  oprabrexex2  6291  mpoexw  6377  rdg0  6552  frecex  6559  1on  6588  2on  6590  3on  6592  4on  6594  2oex  6598  1onn  6687  2onn  6688  3onn  6689  4onn  6690  mapsnf1o2  6864  exmidpw  7099  exmidpw2en  7103  unfiexmid  7109  xpfi  7123  ssfirab  7128  fnfi  7134  iunfidisj  7144  fidcenumlemr  7153  sbthlemi10  7164  ctmlemr  7306  nninfex  7319  exmidonfinlem  7403  acfun  7421  exmidaclem  7422  pw1ne1  7446  ccfunen  7482  nqex  7582  nq0ex  7659  1pr  7773  ltexprlempr  7827  recexprlempr  7851  cauappcvgprlemcl  7872  caucvgprlemcl  7895  caucvgprprlemcl  7923  addvalex  8063  peano1nnnn  8071  peano2nnnn  8072  axcnex  8078  ax1cn  8080  ax1re  8081  pnfxr  8231  mnfxr  8235  inelr  8763  cju  9140  2re  9212  3re  9216  4re  9219  5re  9221  6re  9223  7re  9225  8re  9227  9re  9229  2nn  9304  3nn  9305  4nn  9306  5nn  9307  6nn  9308  7nn  9309  8nn  9310  9nn  9311  nn0ex  9407  nneoor  9581  zeo  9584  deccl  9624  decnncl  9629  numnncl2  9632  decnncl2  9633  numsucc  9649  numma2c  9655  numadd  9656  numaddc  9657  nummul1c  9658  nummul2c  9659  xnegcl  10066  xrex  10090  ioof  10205  uzennn  10697  xnn0nnen  10698  seqex  10710  m1expcl2  10822  faccl  10996  facwordi  11001  faclbnd2  11003  bccl  11028  lswex  11164  crre  11417  remim  11420  absval  11561  climle  11894  climcvg1nlem  11909  iserabs  12035  geo2lim  12076  prodfclim1  12104  fprodle  12200  ere  12230  ege2le3  12231  eftlub  12250  efsep  12251  tan0  12291  ef01bndlem  12316  nn0o  12467  pczpre  12869  pockthi  12930  igz  12946  ennnfonelemj0  13021  ennnfonelem0  13025  ndxarg  13104  ndxslid  13106  strndxid  13109  basendxnn  13137  strle1g  13188  plusgndxnn  13193  2strbasg  13202  2stropg  13203  tsetndxnn  13271  plendxnn  13285  dsndxnn  13300  unifndxnn  13310  rmodislmodlem  14363  rmodislmod  14364  cndsex  14566  znval  14649  znle  14650  znbaslemnn  14652  znbas  14657  znzrhval  14660  psrval  14679  fczpsrbag  14684  setsmsbasg  15202  cnbl0  15257  cnopncntop  15267  cnopn  15268  remet  15271  divcnap  15288  expcn  15292  climcncf  15307  idcncf  15324  expcncf  15332  cnrehmeocntop  15333  hovercncf  15369  plyrecj  15486  sincn  15492  coscn  15493  2logb9irrALT  15697  2irrexpq  15699  2irrexpqap  15701  lgslem4  15731  lgsdir2lem2  15757  edgfndxnn  15858  setsvtx  15901  usgrstrrepeen  16081  bdinex2  16495  bj-inex  16502  012of  16592  2o01f  16593  peano3nninf  16609  cvgcmp2nlemabs  16636  trilpolemisumle  16642