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  4299  onsucelsucexmid  4576  nnpredcl  4669  elvvuni  4737  isarep2  5355  acexmidlemcase  5929  abrexex2  6199  oprabex  6203  oprabrexex2  6205  mpoexw  6289  rdg0  6463  frecex  6470  1on  6499  2on  6501  3on  6503  4on  6504  1onn  6596  2onn  6597  3onn  6598  4onn  6599  mapsnf1o2  6773  exmidpw  6987  exmidpw2en  6991  unfiexmid  6997  xpfi  7011  ssfirab  7015  fnfi  7020  iunfidisj  7030  fidcenumlemr  7039  sbthlemi10  7050  ctmlemr  7192  nninfex  7205  exmidonfinlem  7283  acfun  7301  exmidaclem  7302  pw1ne1  7323  ccfunen  7358  nqex  7458  nq0ex  7535  1pr  7649  ltexprlempr  7703  recexprlempr  7727  cauappcvgprlemcl  7748  caucvgprlemcl  7771  caucvgprprlemcl  7799  addvalex  7939  peano1nnnn  7947  peano2nnnn  7948  axcnex  7954  ax1cn  7956  ax1re  7957  pnfxr  8107  mnfxr  8111  inelr  8639  cju  9016  2re  9088  3re  9092  4re  9095  5re  9097  6re  9099  7re  9101  8re  9103  9re  9105  2nn  9180  3nn  9181  4nn  9182  5nn  9183  6nn  9184  7nn  9185  8nn  9186  9nn  9187  nn0ex  9283  nneoor  9457  zeo  9460  deccl  9500  decnncl  9505  numnncl2  9508  decnncl2  9509  numsucc  9525  numma2c  9531  numadd  9532  numaddc  9533  nummul1c  9534  nummul2c  9535  xnegcl  9936  xrex  9960  ioof  10075  uzennn  10562  xnn0nnen  10563  seqex  10575  m1expcl2  10687  faccl  10861  facwordi  10866  faclbnd2  10868  bccl  10893  crre  11087  remim  11090  absval  11231  climle  11564  climcvg1nlem  11579  iserabs  11705  geo2lim  11746  prodfclim1  11774  fprodle  11870  ere  11900  ege2le3  11901  eftlub  11920  efsep  11921  tan0  11961  ef01bndlem  11986  nn0o  12137  pczpre  12539  pockthi  12600  igz  12616  ennnfonelemj0  12691  ennnfonelem0  12695  ndxarg  12774  ndxslid  12776  strndxid  12779  basendxnn  12807  strle1g  12857  plusgndxnn  12862  2strbasg  12870  2stropg  12871  tsetndxnn  12939  plendxnn  12953  dsndxnn  12968  unifndxnn  12978  rmodislmodlem  14030  rmodislmod  14031  cndsex  14233  znval  14316  znle  14317  znbaslemnn  14319  znbas  14324  znzrhval  14327  psrval  14346  fczpsrbag  14351  setsmsbasg  14869  cnbl0  14924  cnopncntop  14934  cnopn  14935  remet  14938  divcnap  14955  expcn  14959  climcncf  14974  idcncf  14991  expcncf  14999  cnrehmeocntop  15000  hovercncf  15036  plyrecj  15153  sincn  15159  coscn  15160  2logb9irrALT  15364  2irrexpq  15366  2irrexpqap  15368  lgslem4  15398  lgsdir2lem2  15424  bdinex2  15700  bj-inex  15707  012of  15794  2o01f  15795  peano3nninf  15808  cvgcmp2nlemabs  15835  trilpolemisumle  15841