Theorem eqeltri 2250

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

Syntax hints:   = wceq 1353   ∈ wcel 2148

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173

This theorem is referenced by:  eqeltrri  2251  3eltr4i  2259  intab  3875  inex2  4140  vpwex  4181  ord3ex  4192  uniopel  4258  onsucelsucexmid  4531  nnpredcl  4624  elvvuni  4692  isarep2  5305  acexmidlemcase  5873  abrexex2  6128  oprabex  6132  oprabrexex2  6134  mpoexw  6217  rdg0  6391  frecex  6398  1on  6427  2on  6429  3on  6431  4on  6432  1onn  6524  2onn  6525  3onn  6526  4onn  6527  mapsnf1o2  6699  exmidpw  6911  unfiexmid  6920  xpfi  6932  ssfirab  6936  fnfi  6939  iunfidisj  6948  fidcenumlemr  6957  sbthlemi10  6968  ctmlemr  7110  nninfex  7123  exmidonfinlem  7195  acfun  7209  exmidaclem  7210  pw1ne1  7231  ccfunen  7266  nqex  7365  nq0ex  7442  1pr  7556  ltexprlempr  7610  recexprlempr  7634  cauappcvgprlemcl  7655  caucvgprlemcl  7678  caucvgprprlemcl  7706  addvalex  7846  peano1nnnn  7854  peano2nnnn  7855  axcnex  7861  ax1cn  7863  ax1re  7864  pnfxr  8013  mnfxr  8017  inelr  8544  cju  8921  2re  8992  3re  8996  4re  8999  5re  9001  6re  9003  7re  9005  8re  9007  9re  9009  2nn  9083  3nn  9084  4nn  9085  5nn  9086  6nn  9087  7nn  9088  8nn  9089  9nn  9090  nn0ex  9185  nneoor  9358  zeo  9361  deccl  9401  decnncl  9406  numnncl2  9409  decnncl2  9410  numsucc  9426  numma2c  9432  numadd  9433  numaddc  9434  nummul1c  9435  nummul2c  9436  xnegcl  9835  xrex  9859  ioof  9974  uzennn  10439  seqex  10450  m1expcl2  10545  faccl  10718  facwordi  10723  faclbnd2  10725  bccl  10750  crre  10869  remim  10872  absval  11013  climle  11345  climcvg1nlem  11360  iserabs  11486  geo2lim  11527  prodfclim1  11555  fprodle  11651  ere  11681  ege2le3  11682  eftlub  11701  efsep  11702  tan0  11742  ef01bndlem  11767  nn0o  11915  pczpre  12300  pockthi  12359  igz  12375  ennnfonelemj0  12405  ennnfonelem0  12409  ndxarg  12488  ndxslid  12490  strndxid  12493  basendxnn  12521  strle1g  12568  plusgndxnn  12573  2strbasg  12581  2stropg  12582  tsetndxnn  12650  plendxnn  12664  dsndxnn  12675  unifndxnn  12685  rmodislmodlem  13451  rmodislmod  13452  setsmsbasg  14140  cnbl0  14195  cnopncntop  14198  remet  14201  divcnap  14216  climcncf  14232  expcncf  14253  cnrehmeocntop  14254  sincn  14351  coscn  14352  2logb9irrALT  14553  2irrexpq  14555  2irrexpqap  14557  lgslem4  14565  lgsdir2lem2  14591  bdinex2  14813  bj-inex  14820  012of  14907  2o01f  14908  peano3nninf  14918  cvgcmp2nlemabs  14942  trilpolemisumle  14948