Theorem eqeltri 2279

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

Syntax hints:   = wceq 1373   ∈ wcel 2177

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-cleq 2199  df-clel 2202

This theorem is referenced by:  eqeltrri  2280  3eltr4i  2288  intab  3920  inex2  4187  vpwex  4231  ord3ex  4242  uniopel  4309  onsucelsucexmid  4586  nnpredcl  4679  elvvuni  4747  isarep2  5370  acexmidlemcase  5952  abrexex2  6222  oprabex  6226  oprabrexex2  6228  mpoexw  6312  rdg0  6486  frecex  6493  1on  6522  2on  6524  3on  6526  4on  6527  1onn  6619  2onn  6620  3onn  6621  4onn  6622  mapsnf1o2  6796  exmidpw  7020  exmidpw2en  7024  unfiexmid  7030  xpfi  7044  ssfirab  7048  fnfi  7053  iunfidisj  7063  fidcenumlemr  7072  sbthlemi10  7083  ctmlemr  7225  nninfex  7238  exmidonfinlem  7317  acfun  7335  exmidaclem  7336  pw1ne1  7360  ccfunen  7396  nqex  7496  nq0ex  7573  1pr  7687  ltexprlempr  7741  recexprlempr  7765  cauappcvgprlemcl  7786  caucvgprlemcl  7809  caucvgprprlemcl  7837  addvalex  7977  peano1nnnn  7985  peano2nnnn  7986  axcnex  7992  ax1cn  7994  ax1re  7995  pnfxr  8145  mnfxr  8149  inelr  8677  cju  9054  2re  9126  3re  9130  4re  9133  5re  9135  6re  9137  7re  9139  8re  9141  9re  9143  2nn  9218  3nn  9219  4nn  9220  5nn  9221  6nn  9222  7nn  9223  8nn  9224  9nn  9225  nn0ex  9321  nneoor  9495  zeo  9498  deccl  9538  decnncl  9543  numnncl2  9546  decnncl2  9547  numsucc  9563  numma2c  9569  numadd  9570  numaddc  9571  nummul1c  9572  nummul2c  9573  xnegcl  9974  xrex  9998  ioof  10113  uzennn  10603  xnn0nnen  10604  seqex  10616  m1expcl2  10728  faccl  10902  facwordi  10907  faclbnd2  10909  bccl  10934  lswex  11067  crre  11243  remim  11246  absval  11387  climle  11720  climcvg1nlem  11735  iserabs  11861  geo2lim  11902  prodfclim1  11930  fprodle  12026  ere  12056  ege2le3  12057  eftlub  12076  efsep  12077  tan0  12117  ef01bndlem  12142  nn0o  12293  pczpre  12695  pockthi  12756  igz  12772  ennnfonelemj0  12847  ennnfonelem0  12851  ndxarg  12930  ndxslid  12932  strndxid  12935  basendxnn  12963  strle1g  13013  plusgndxnn  13018  2strbasg  13027  2stropg  13028  tsetndxnn  13096  plendxnn  13110  dsndxnn  13125  unifndxnn  13135  rmodislmodlem  14187  rmodislmod  14188  cndsex  14390  znval  14473  znle  14474  znbaslemnn  14476  znbas  14481  znzrhval  14484  psrval  14503  fczpsrbag  14508  setsmsbasg  15026  cnbl0  15081  cnopncntop  15091  cnopn  15092  remet  15095  divcnap  15112  expcn  15116  climcncf  15131  idcncf  15148  expcncf  15156  cnrehmeocntop  15157  hovercncf  15193  plyrecj  15310  sincn  15316  coscn  15317  2logb9irrALT  15521  2irrexpq  15523  2irrexpqap  15525  lgslem4  15555  lgsdir2lem2  15581  edgfndxnn  15682  bdinex2  15974  bj-inex  15981  012of  16069  2o01f  16070  peano3nninf  16085  cvgcmp2nlemabs  16112  trilpolemisumle  16118