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  3873  inex2  4138  vpwex  4179  ord3ex  4190  uniopel  4256  onsucelsucexmid  4529  nnpredcl  4622  elvvuni  4690  isarep2  5303  acexmidlemcase  5869  abrexex2  6124  oprabex  6128  oprabrexex2  6130  mpoexw  6213  rdg0  6387  frecex  6394  1on  6423  2on  6425  3on  6427  4on  6428  1onn  6520  2onn  6521  3onn  6522  4onn  6523  mapsnf1o2  6695  exmidpw  6907  unfiexmid  6916  xpfi  6928  ssfirab  6932  fnfi  6935  iunfidisj  6944  fidcenumlemr  6953  sbthlemi10  6964  ctmlemr  7106  nninfex  7119  exmidonfinlem  7191  acfun  7205  exmidaclem  7206  pw1ne1  7227  ccfunen  7262  nqex  7361  nq0ex  7438  1pr  7552  ltexprlempr  7606  recexprlempr  7630  cauappcvgprlemcl  7651  caucvgprlemcl  7674  caucvgprprlemcl  7702  addvalex  7842  peano1nnnn  7850  peano2nnnn  7851  axcnex  7857  ax1cn  7859  ax1re  7860  pnfxr  8009  mnfxr  8013  inelr  8540  cju  8917  2re  8988  3re  8992  4re  8995  5re  8997  6re  8999  7re  9001  8re  9003  9re  9005  2nn  9079  3nn  9080  4nn  9081  5nn  9082  6nn  9083  7nn  9084  8nn  9085  9nn  9086  nn0ex  9181  nneoor  9354  zeo  9357  deccl  9397  decnncl  9402  numnncl2  9405  decnncl2  9406  numsucc  9422  numma2c  9428  numadd  9429  numaddc  9430  nummul1c  9431  nummul2c  9432  xnegcl  9831  xrex  9855  ioof  9970  uzennn  10435  seqex  10446  m1expcl2  10541  faccl  10714  facwordi  10719  faclbnd2  10721  bccl  10746  crre  10865  remim  10868  absval  11009  climle  11341  climcvg1nlem  11356  iserabs  11482  geo2lim  11523  prodfclim1  11551  fprodle  11647  ere  11677  ege2le3  11678  eftlub  11697  efsep  11698  tan0  11738  ef01bndlem  11763  nn0o  11911  pczpre  12296  pockthi  12355  igz  12371  ennnfonelemj0  12401  ennnfonelem0  12405  ndxarg  12484  ndxslid  12486  strndxid  12489  basendxnn  12517  strle1g  12564  plusgndxnn  12569  2strbasg  12577  2stropg  12578  tsetndxnn  12643  plendxnn  12657  dsndxnn  12668  unifndxnn  12678  setsmsbasg  13949  cnbl0  14004  cnopncntop  14007  remet  14010  divcnap  14025  climcncf  14041  expcncf  14062  cnrehmeocntop  14063  sincn  14160  coscn  14161  2logb9irrALT  14362  2irrexpq  14364  2irrexpqap  14366  lgslem4  14374  lgsdir2lem2  14400  bdinex2  14622  bj-inex  14629  012of  14715  2o01f  14716  peano3nninf  14726  cvgcmp2nlemabs  14750  trilpolemisumle  14756