Theorem eqeltri 2302

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

Syntax hints:   = wceq 1395   ∈ wcel 2200

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

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

This theorem is referenced by:  eqeltrri  2303  3eltr4i  2311  intab  3955  inex2  4222  vpwex  4267  ord3ex  4278  uniopel  4347  onsucelsucexmid  4626  nnpredcl  4719  elvvuni  4788  isarep2  5414  acexmidlemcase  6008  abrexex2  6281  oprabex  6285  oprabrexex2  6287  mpoexw  6373  rdg0  6548  frecex  6555  1on  6584  2on  6586  3on  6588  4on  6590  2oex  6594  1onn  6683  2onn  6684  3onn  6685  4onn  6686  mapsnf1o2  6860  exmidpw  7093  exmidpw2en  7097  unfiexmid  7103  xpfi  7117  ssfirab  7121  fnfi  7126  iunfidisj  7136  fidcenumlemr  7145  sbthlemi10  7156  ctmlemr  7298  nninfex  7311  exmidonfinlem  7394  acfun  7412  exmidaclem  7413  pw1ne1  7437  ccfunen  7473  nqex  7573  nq0ex  7650  1pr  7764  ltexprlempr  7818  recexprlempr  7842  cauappcvgprlemcl  7863  caucvgprlemcl  7886  caucvgprprlemcl  7914  addvalex  8054  peano1nnnn  8062  peano2nnnn  8063  axcnex  8069  ax1cn  8071  ax1re  8072  pnfxr  8222  mnfxr  8226  inelr  8754  cju  9131  2re  9203  3re  9207  4re  9210  5re  9212  6re  9214  7re  9216  8re  9218  9re  9220  2nn  9295  3nn  9296  4nn  9297  5nn  9298  6nn  9299  7nn  9300  8nn  9301  9nn  9302  nn0ex  9398  nneoor  9572  zeo  9575  deccl  9615  decnncl  9620  numnncl2  9623  decnncl2  9624  numsucc  9640  numma2c  9646  numadd  9647  numaddc  9648  nummul1c  9649  nummul2c  9650  xnegcl  10057  xrex  10081  ioof  10196  uzennn  10688  xnn0nnen  10689  seqex  10701  m1expcl2  10813  faccl  10987  facwordi  10992  faclbnd2  10994  bccl  11019  lswex  11155  crre  11408  remim  11411  absval  11552  climle  11885  climcvg1nlem  11900  iserabs  12026  geo2lim  12067  prodfclim1  12095  fprodle  12191  ere  12221  ege2le3  12222  eftlub  12241  efsep  12242  tan0  12282  ef01bndlem  12307  nn0o  12458  pczpre  12860  pockthi  12921  igz  12937  ennnfonelemj0  13012  ennnfonelem0  13016  ndxarg  13095  ndxslid  13097  strndxid  13100  basendxnn  13128  strle1g  13179  plusgndxnn  13184  2strbasg  13193  2stropg  13194  tsetndxnn  13262  plendxnn  13276  dsndxnn  13291  unifndxnn  13301  rmodislmodlem  14354  rmodislmod  14355  cndsex  14557  znval  14640  znle  14641  znbaslemnn  14643  znbas  14648  znzrhval  14651  psrval  14670  fczpsrbag  14675  setsmsbasg  15193  cnbl0  15248  cnopncntop  15258  cnopn  15259  remet  15262  divcnap  15279  expcn  15283  climcncf  15298  idcncf  15315  expcncf  15323  cnrehmeocntop  15324  hovercncf  15360  plyrecj  15477  sincn  15483  coscn  15484  2logb9irrALT  15688  2irrexpq  15690  2irrexpqap  15692  lgslem4  15722  lgsdir2lem2  15748  edgfndxnn  15849  setsvtx  15892  usgrstrrepeen  16070  bdinex2  16431  bj-inex  16438  012of  16528  2o01f  16529  peano3nninf  16545  cvgcmp2nlemabs  16572  trilpolemisumle  16578