Theorem eqeltri 2238

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

Syntax hints:   = wceq 1343   ∈ wcel 2136

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 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158  df-clel 2161

This theorem is referenced by:  eqeltrri  2239  3eltr4i  2247  intab  3852  inex2  4116  vpwex  4157  ord3ex  4168  uniopel  4233  onsucelsucexmid  4506  nnpredcl  4599  elvvuni  4667  isarep2  5274  acexmidlemcase  5836  abrexex2  6089  oprabex  6093  oprabrexex2  6095  rdg0  6351  frecex  6358  1on  6387  2on  6389  3on  6391  4on  6392  1onn  6484  2onn  6485  3onn  6486  4onn  6487  mapsnf1o2  6658  exmidpw  6870  unfiexmid  6879  xpfi  6891  ssfirab  6895  fnfi  6898  iunfidisj  6907  fidcenumlemr  6916  sbthlemi10  6927  ctmlemr  7069  nninfex  7082  exmidonfinlem  7145  acfun  7159  exmidaclem  7160  pw1ne1  7181  ccfunen  7201  nqex  7300  nq0ex  7377  1pr  7491  ltexprlempr  7545  recexprlempr  7569  cauappcvgprlemcl  7590  caucvgprlemcl  7613  caucvgprprlemcl  7641  addvalex  7781  peano1nnnn  7789  peano2nnnn  7790  axcnex  7796  ax1cn  7798  ax1re  7799  pnfxr  7947  mnfxr  7951  inelr  8478  cju  8852  2re  8923  3re  8927  4re  8930  5re  8932  6re  8934  7re  8936  8re  8938  9re  8940  2nn  9014  3nn  9015  4nn  9016  5nn  9017  6nn  9018  7nn  9019  8nn  9020  9nn  9021  nn0ex  9116  nneoor  9289  zeo  9292  deccl  9332  decnncl  9337  numnncl2  9340  decnncl2  9341  numsucc  9357  numma2c  9363  numadd  9364  numaddc  9365  nummul1c  9366  nummul2c  9367  xnegcl  9764  xrex  9788  ioof  9903  uzennn  10367  seqex  10378  m1expcl2  10473  faccl  10644  facwordi  10649  faclbnd2  10651  bccl  10676  crre  10795  remim  10798  absval  10939  climle  11271  climcvg1nlem  11286  iserabs  11412  geo2lim  11453  prodfclim1  11481  fprodle  11577  ere  11607  ege2le3  11608  eftlub  11627  efsep  11628  tan0  11668  ef01bndlem  11693  nn0o  11840  pczpre  12225  pockthi  12284  igz  12300  ennnfonelemj0  12330  ennnfonelem0  12334  ndxarg  12413  ndxslid  12415  strndxid  12418  basendxnn  12445  strle1g  12480  2strbasg  12491  2stropg  12492  setsmsbasg  13079  cnbl0  13134  cnopncntop  13137  remet  13140  divcnap  13155  climcncf  13171  expcncf  13192  cnrehmeocntop  13193  sincn  13290  coscn  13291  2logb9irrALT  13492  2irrexpq  13494  2irrexpqap  13496  lgslem4  13504  lgsdir2lem2  13530  bdinex2  13742  bj-inex  13749  012of  13835  2o01f  13836  peano3nninf  13847  cvgcmp2nlemabs  13871  trilpolemisumle  13877