Theorem eqeltri 2269

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

Syntax hints:   = wceq 1364   ∈ wcel 2167

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-clel 2192

This theorem is referenced by:  eqeltrri  2270  3eltr4i  2278  intab  3904  inex2  4169  vpwex  4213  ord3ex  4224  uniopel  4290  onsucelsucexmid  4567  nnpredcl  4660  elvvuni  4728  isarep2  5346  acexmidlemcase  5920  abrexex2  6190  oprabex  6194  oprabrexex2  6196  mpoexw  6280  rdg0  6454  frecex  6461  1on  6490  2on  6492  3on  6494  4on  6495  1onn  6587  2onn  6588  3onn  6589  4onn  6590  mapsnf1o2  6764  exmidpw  6978  exmidpw2en  6982  unfiexmid  6988  xpfi  7002  ssfirab  7006  fnfi  7011  iunfidisj  7021  fidcenumlemr  7030  sbthlemi10  7041  ctmlemr  7183  nninfex  7196  exmidonfinlem  7274  acfun  7292  exmidaclem  7293  pw1ne1  7314  ccfunen  7349  nqex  7449  nq0ex  7526  1pr  7640  ltexprlempr  7694  recexprlempr  7718  cauappcvgprlemcl  7739  caucvgprlemcl  7762  caucvgprprlemcl  7790  addvalex  7930  peano1nnnn  7938  peano2nnnn  7939  axcnex  7945  ax1cn  7947  ax1re  7948  pnfxr  8098  mnfxr  8102  inelr  8630  cju  9007  2re  9079  3re  9083  4re  9086  5re  9088  6re  9090  7re  9092  8re  9094  9re  9096  2nn  9171  3nn  9172  4nn  9173  5nn  9174  6nn  9175  7nn  9176  8nn  9177  9nn  9178  nn0ex  9274  nneoor  9447  zeo  9450  deccl  9490  decnncl  9495  numnncl2  9498  decnncl2  9499  numsucc  9515  numma2c  9521  numadd  9522  numaddc  9523  nummul1c  9524  nummul2c  9525  xnegcl  9926  xrex  9950  ioof  10065  uzennn  10547  xnn0nnen  10548  seqex  10560  m1expcl2  10672  faccl  10846  facwordi  10851  faclbnd2  10853  bccl  10878  crre  11041  remim  11044  absval  11185  climle  11518  climcvg1nlem  11533  iserabs  11659  geo2lim  11700  prodfclim1  11728  fprodle  11824  ere  11854  ege2le3  11855  eftlub  11874  efsep  11875  tan0  11915  ef01bndlem  11940  nn0o  12091  pczpre  12493  pockthi  12554  igz  12570  ennnfonelemj0  12645  ennnfonelem0  12649  ndxarg  12728  ndxslid  12730  strndxid  12733  basendxnn  12761  strle1g  12811  plusgndxnn  12816  2strbasg  12824  2stropg  12825  tsetndxnn  12893  plendxnn  12907  dsndxnn  12922  unifndxnn  12932  rmodislmodlem  13984  rmodislmod  13985  cndsex  14187  znval  14270  znle  14271  znbaslemnn  14273  znbas  14278  znzrhval  14281  psrval  14300  fczpsrbag  14305  setsmsbasg  14823  cnbl0  14878  cnopncntop  14888  cnopn  14889  remet  14892  divcnap  14909  expcn  14913  climcncf  14928  idcncf  14945  expcncf  14953  cnrehmeocntop  14954  hovercncf  14990  plyrecj  15107  sincn  15113  coscn  15114  2logb9irrALT  15318  2irrexpq  15320  2irrexpqap  15322  lgslem4  15352  lgsdir2lem2  15378  bdinex2  15654  bj-inex  15661  012of  15748  2o01f  15749  peano3nninf  15762  cvgcmp2nlemabs  15789  trilpolemisumle  15795