Theorem eqeltri 2212

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 2205	. 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 2121

This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135

This theorem is referenced by:  eqeltrri  2213  3eltr4i  2221  intab  3800  inex2  4063  vpwex  4103  ord3ex  4114  uniopel  4178  onsucelsucexmid  4445  nnpredcl  4536  elvvuni  4603  isarep2  5210  acexmidlemcase  5769  abrexex2  6022  oprabex  6026  oprabrexex2  6028  rdg0  6284  frecex  6291  1on  6320  2on  6322  3on  6324  4on  6325  1onn  6416  2onn  6417  3onn  6418  4onn  6419  mapsnf1o2  6590  exmidpw  6802  unfiexmid  6806  xpfi  6818  ssfirab  6822  fnfi  6825  iunfidisj  6834  fidcenumlemr  6843  sbthlemi10  6854  ctmlemr  6993  exmidonfinlem  7049  acfun  7063  exmidaclem  7064  ccfunen  7079  nqex  7171  nq0ex  7248  1pr  7362  ltexprlempr  7416  recexprlempr  7440  cauappcvgprlemcl  7461  caucvgprlemcl  7484  caucvgprprlemcl  7512  addvalex  7652  peano1nnnn  7660  peano2nnnn  7661  axcnex  7667  ax1cn  7669  ax1re  7670  pnfxr  7818  mnfxr  7822  inelr  8346  cju  8719  2re  8790  3re  8794  4re  8797  5re  8799  6re  8801  7re  8803  8re  8805  9re  8807  2nn  8881  3nn  8882  4nn  8883  5nn  8884  6nn  8885  7nn  8886  8nn  8887  9nn  8888  nn0ex  8983  nneoor  9153  zeo  9156  deccl  9196  decnncl  9201  numnncl2  9204  decnncl2  9205  numsucc  9221  numma2c  9227  numadd  9228  numaddc  9229  nummul1c  9230  nummul2c  9231  xnegcl  9615  xrex  9639  ioof  9754  uzennn  10209  seqex  10220  m1expcl2  10315  faccl  10481  facwordi  10486  faclbnd2  10488  bccl  10513  crre  10629  remim  10632  absval  10773  climle  11103  climcvg1nlem  11118  iserabs  11244  geo2lim  11285  prodfclim1  11313  ere  11376  ege2le3  11377  eftlub  11396  efsep  11397  tan0  11438  ef01bndlem  11463  nn0o  11604  ennnfonelemj0  11914  ennnfonelem0  11918  ndxarg  11982  ndxslid  11984  strndxid  11987  basendxnn  12014  strle1g  12049  2strbasg  12060  2stropg  12061  setsmsbasg  12648  cnbl0  12703  cnopncntop  12706  remet  12709  divcnap  12724  climcncf  12740  expcncf  12761  cnrehmeocntop  12762  sincn  12858  coscn  12859  bdinex2  13098  bj-inex  13105  peano3nninf  13201  nninfex  13205  isomninnlem  13225  cvgcmp2nlemabs  13227  trilpolemisumle  13231