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  5872  abrexex2  6127  oprabex  6131  oprabrexex2  6133  mpoexw  6216  rdg0  6390  frecex  6397  1on  6426  2on  6428  3on  6430  4on  6431  1onn  6523  2onn  6524  3onn  6525  4onn  6526  mapsnf1o2  6698  exmidpw  6910  unfiexmid  6919  xpfi  6931  ssfirab  6935  fnfi  6938  iunfidisj  6947  fidcenumlemr  6956  sbthlemi10  6967  ctmlemr  7109  nninfex  7122  exmidonfinlem  7194  acfun  7208  exmidaclem  7209  pw1ne1  7230  ccfunen  7265  nqex  7364  nq0ex  7441  1pr  7555  ltexprlempr  7609  recexprlempr  7633  cauappcvgprlemcl  7654  caucvgprlemcl  7677  caucvgprprlemcl  7705  addvalex  7845  peano1nnnn  7853  peano2nnnn  7854  axcnex  7860  ax1cn  7862  ax1re  7863  pnfxr  8012  mnfxr  8016  inelr  8543  cju  8920  2re  8991  3re  8995  4re  8998  5re  9000  6re  9002  7re  9004  8re  9006  9re  9008  2nn  9082  3nn  9083  4nn  9084  5nn  9085  6nn  9086  7nn  9087  8nn  9088  9nn  9089  nn0ex  9184  nneoor  9357  zeo  9360  deccl  9400  decnncl  9405  numnncl2  9408  decnncl2  9409  numsucc  9425  numma2c  9431  numadd  9432  numaddc  9433  nummul1c  9434  nummul2c  9435  xnegcl  9834  xrex  9858  ioof  9973  uzennn  10438  seqex  10449  m1expcl2  10544  faccl  10717  facwordi  10722  faclbnd2  10724  bccl  10749  crre  10868  remim  10871  absval  11012  climle  11344  climcvg1nlem  11359  iserabs  11485  geo2lim  11526  prodfclim1  11554  fprodle  11650  ere  11680  ege2le3  11681  eftlub  11700  efsep  11701  tan0  11741  ef01bndlem  11766  nn0o  11914  pczpre  12299  pockthi  12358  igz  12374  ennnfonelemj0  12404  ennnfonelem0  12408  ndxarg  12487  ndxslid  12489  strndxid  12492  basendxnn  12520  strle1g  12567  plusgndxnn  12572  2strbasg  12580  2stropg  12581  tsetndxnn  12649  plendxnn  12663  dsndxnn  12674  unifndxnn  12684  rmodislmodlem  13445  rmodislmod  13446  setsmsbasg  14018  cnbl0  14073  cnopncntop  14076  remet  14079  divcnap  14094  climcncf  14110  expcncf  14131  cnrehmeocntop  14132  sincn  14229  coscn  14230  2logb9irrALT  14431  2irrexpq  14433  2irrexpqap  14435  lgslem4  14443  lgsdir2lem2  14469  bdinex2  14691  bj-inex  14698  012of  14784  2o01f  14785  peano3nninf  14795  cvgcmp2nlemabs  14819  trilpolemisumle  14825