Theorem eqeltri 2304

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

Syntax hints:   = wceq 1398   ∈ wcel 2202

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227

This theorem is referenced by:  eqeltrri  2305  3eltr4i  2313  intab  3962  inex2  4229  vpwex  4275  ord3ex  4286  uniopel  4355  onsucelsucexmid  4634  nnpredcl  4727  elvvuni  4796  isarep2  5424  acexmidlemcase  6023  abrexex2  6295  oprabex  6299  oprabrexex2  6301  mpoexw  6387  rdg0  6596  frecex  6603  1on  6632  2on  6634  3on  6636  4on  6638  2oex  6642  1onn  6731  2onn  6732  3onn  6733  4onn  6734  mapsnf1o2  6908  exmidpw  7143  exmidpw2en  7147  unfiexmid  7153  xpfi  7167  ssfirab  7172  fnfi  7178  iunfidisj  7188  fidcenumlemr  7197  sbthlemi10  7208  ctmlemr  7350  nninfex  7363  exmidonfinlem  7447  acfun  7465  exmidaclem  7466  pw1ne1  7490  ccfunen  7526  nqex  7626  nq0ex  7703  1pr  7817  ltexprlempr  7871  recexprlempr  7895  cauappcvgprlemcl  7916  caucvgprlemcl  7939  caucvgprprlemcl  7967  addvalex  8107  peano1nnnn  8115  peano2nnnn  8116  axcnex  8122  ax1cn  8124  ax1re  8125  pnfxr  8274  mnfxr  8278  inelr  8806  cju  9183  2re  9255  3re  9259  4re  9262  5re  9264  6re  9266  7re  9268  8re  9270  9re  9272  2nn  9347  3nn  9348  4nn  9349  5nn  9350  6nn  9351  7nn  9352  8nn  9353  9nn  9354  nn0ex  9450  nneoor  9626  zeo  9629  deccl  9669  decnncl  9674  numnncl2  9677  decnncl2  9678  numsucc  9694  numma2c  9700  numadd  9701  numaddc  9702  nummul1c  9703  nummul2c  9704  xnegcl  10111  xrex  10135  ioof  10250  uzennn  10744  xnn0nnen  10745  seqex  10757  m1expcl2  10869  faccl  11043  facwordi  11048  faclbnd2  11050  bccl  11075  lswex  11214  crre  11480  remim  11483  absval  11624  climle  11957  climcvg1nlem  11972  iserabs  12099  geo2lim  12140  prodfclim1  12168  fprodle  12264  ere  12294  ege2le3  12295  eftlub  12314  efsep  12315  tan0  12355  ef01bndlem  12380  nn0o  12531  pczpre  12933  pockthi  12994  igz  13010  ennnfonelemj0  13085  ennnfonelem0  13089  ndxarg  13168  ndxslid  13170  strndxid  13173  basendxnn  13201  strle1g  13252  plusgndxnn  13257  2strbasg  13266  2stropg  13267  tsetndxnn  13335  plendxnn  13349  dsndxnn  13364  unifndxnn  13374  rmodislmodlem  14429  rmodislmod  14430  cndsex  14632  znval  14715  znle  14716  znbaslemnn  14718  znbas  14723  znzrhval  14726  psrval  14745  fczpsrbag  14750  setsmsbasg  15273  cnbl0  15328  cnopncntop  15338  cnopn  15339  remet  15342  divcnap  15359  expcn  15363  climcncf  15378  idcncf  15395  expcncf  15403  cnrehmeocntop  15404  hovercncf  15440  plyrecj  15557  sincn  15563  coscn  15564  2logb9irrALT  15768  2irrexpq  15770  2irrexpqap  15772  lgslem4  15805  lgsdir2lem2  15831  edgfndxnn  15932  setsvtx  15975  usgrstrrepeen  16155  eulerpathprum  16404  konigsbergumgr  16411  konigsberglem5  16416  konigsberg  16417  bdinex2  16599  bj-inex  16606  012of  16696  2o01f  16697  peano3nninf  16716  cvgcmp2nlemabs  16747  trilpolemisumle  16753