Theorem eqeltri 2210

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

Syntax hints:   = wceq 1331   ∈ wcel 1480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-cleq 2130  df-clel 2133

This theorem is referenced by:  eqeltrri  2211  3eltr4i  2219  intab  3795  inex2  4058  vpwex  4098  ord3ex  4109  uniopel  4173  onsucelsucexmid  4440  nnpredcl  4531  elvvuni  4598  isarep2  5205  acexmidlemcase  5762  abrexex2  6015  oprabex  6019  oprabrexex2  6021  rdg0  6277  frecex  6284  1on  6313  2on  6315  3on  6317  4on  6318  1onn  6409  2onn  6410  3onn  6411  4onn  6412  mapsnf1o2  6583  exmidpw  6795  unfiexmid  6799  xpfi  6811  ssfirab  6815  fnfi  6818  iunfidisj  6827  fidcenumlemr  6836  sbthlemi10  6847  ctmlemr  6986  exmidonfinlem  7042  acfun  7056  exmidaclem  7057  ccfunen  7072  nqex  7164  nq0ex  7241  1pr  7355  ltexprlempr  7409  recexprlempr  7433  cauappcvgprlemcl  7454  caucvgprlemcl  7477  caucvgprprlemcl  7505  addvalex  7645  peano1nnnn  7653  peano2nnnn  7654  axcnex  7660  ax1cn  7662  ax1re  7663  pnfxr  7811  mnfxr  7815  inelr  8339  cju  8712  2re  8783  3re  8787  4re  8790  5re  8792  6re  8794  7re  8796  8re  8798  9re  8800  2nn  8874  3nn  8875  4nn  8876  5nn  8877  6nn  8878  7nn  8879  8nn  8880  9nn  8881  nn0ex  8976  nneoor  9146  zeo  9149  deccl  9189  decnncl  9194  numnncl2  9197  decnncl2  9198  numsucc  9214  numma2c  9220  numadd  9221  numaddc  9222  nummul1c  9223  nummul2c  9224  xnegcl  9608  xrex  9632  ioof  9747  uzennn  10202  seqex  10213  m1expcl2  10308  faccl  10474  facwordi  10479  faclbnd2  10481  bccl  10506  crre  10622  remim  10625  absval  10766  climle  11096  climcvg1nlem  11111  iserabs  11237  geo2lim  11278  prodfclim1  11306  ere  11365  ege2le3  11366  eftlub  11385  efsep  11386  tan0  11427  ef01bndlem  11452  nn0o  11593  ennnfonelemj0  11903  ennnfonelem0  11907  ndxarg  11971  ndxslid  11973  strndxid  11976  basendxnn  12003  strle1g  12038  2strbasg  12049  2stropg  12050  setsmsbasg  12637  cnbl0  12692  cnopncntop  12695  remet  12698  divcnap  12713  climcncf  12729  expcncf  12750  cnrehmeocntop  12751  sincn  12847  coscn  12848  bdinex2  13087  bj-inex  13094  peano3nninf  13190  nninfex  13194  isomninnlem  13214  cvgcmp2nlemabs  13216  trilpolemisumle  13220