Theorem eqeltri 2307

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

Syntax hints:   = wceq 1398   ∈ wcel 2205

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 2216

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-clel 2230

This theorem is referenced by:  eqeltrri  2308  3eltr4i  2316  intab  3983  inex2  4250  vpwex  4297  ord3ex  4308  vsnex  4329  uniopel  4378  onsucelsucexmid  4657  nnpredcl  4750  elvvuni  4819  isarep2  5448  acexmidlemcase  6053  abrexex2  6326  oprabex  6334  oprabrexex2  6336  mpoexw  6422  rdg0  6631  frecex  6638  1on  6667  2on  6669  3on  6671  4on  6673  2oex  6677  1onn  6766  2onn  6767  3onn  6768  4onn  6769  mapsnf1o2  6944  exmidpw  7181  exmidpw2en  7185  unfiexmid  7191  xpfi  7205  ssfirab  7210  fnfi  7216  iunfidisj  7226  fidcenumlemr  7238  sbthlemi10  7249  fczfsuppd  7263  ctmlemr  7412  nninfex  7425  exmidonfinlem  7509  acfun  7527  exmidaclem  7528  pw1ne1  7552  ccfunen  7594  nqex  7694  nq0ex  7771  1pr  7885  ltexprlempr  7939  recexprlempr  7963  cauappcvgprlemcl  7984  caucvgprlemcl  8007  caucvgprprlemcl  8035  addvalex  8175  peano1nnnn  8183  peano2nnnn  8184  axcnex  8190  ax1cn  8192  ax1re  8193  pnfxr  8342  mnfxr  8346  inelr  8875  cju  9252  2re  9324  3re  9328  4re  9331  5re  9333  6re  9335  7re  9337  8re  9339  9re  9341  2nn  9416  3nn  9417  4nn  9418  5nn  9419  6nn  9420  7nn  9421  8nn  9422  9nn  9423  nn0ex  9519  nneoor  9698  zeo  9701  deccl  9741  decnncl  9746  numnncl2  9749  decnncl2  9750  numsucc  9766  numma2c  9772  numadd  9773  numaddc  9774  nummul1c  9775  nummul2c  9776  xnegcl  10184  xrex  10208  ioof  10323  uzennn  10822  xnn0nnen  10823  seqex  10835  m1expcl2  10947  faccl  11122  facwordi  11127  faclbnd2  11129  bccl  11154  lswex  11301  crre  11567  remim  11570  absval  11711  climle  12044  climcvg1nlem  12059  iserabs  12186  geo2lim  12227  prodfclim1  12255  fprodle  12351  ere  12381  ege2le3  12382  eftlub  12401  efsep  12402  tan0  12442  ef01bndlem  12467  nn0o  12618  pczpre  13020  pockthi  13081  igz  13097  ballotfilemofi  13163  ballotfilemonn  13165  ballotfilemefi  13181  ballotfilem7  13223  ennnfonelemj0  13236  ennnfonelem0  13240  ndxarg  13319  ndxslid  13321  strndxid  13324  basendxnn  13352  strle1g  13403  plusgndxnn  13408  2strbasg  13417  2stropg  13418  tsetndxnn  13486  plendxnn  13500  dsndxnn  13515  unifndxnn  13525  rmodislmodlem  14624  rmodislmod  14625  cndsex  14827  znval  14910  znle  14911  znbaslemnn  14913  znbas  14918  znzrhval  14921  psrval  14940  fczpsrbag  14946  setsmsbasg  15470  cnbl0  15525  cnopncntop  15535  cnopn  15536  remet  15539  divcnap  15556  expcn  15560  climcncf  15575  idcncf  15592  expcncf  15600  cnrehmeocntop  15601  hovercncf  15637  plyrecj  15754  sincn  15760  coscn  15761  2logb9irrALT  15965  2irrexpq  15967  2irrexpqap  15969  lgslem4  16002  lgsdir2lem2  16028  edgfndxnn  16129  setsvtx  16172  usgrstrrepeen  16352  eulerpathprum  16601  konigsbergumgr  16608  konigsberglem5  16613  konigsberg  16614  bdinex2  16796  bj-inex  16803  012of  16893  2o01f  16894  peano3nninf  16911  cvgcmp2nlemabs  16942  trilpolemisumle  16948