Theorem eqeltri 2302

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

Syntax hints:   = wceq 1395   ∈ wcel 2200

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  eqeltrri  2303  3eltr4i  2311  intab  3951  inex2  4218  vpwex  4262  ord3ex  4273  uniopel  4342  onsucelsucexmid  4621  nnpredcl  4714  elvvuni  4782  isarep2  5407  acexmidlemcase  5995  abrexex2  6267  oprabex  6271  oprabrexex2  6273  mpoexw  6357  rdg0  6531  frecex  6538  1on  6567  2on  6569  3on  6571  4on  6572  1onn  6664  2onn  6665  3onn  6666  4onn  6667  mapsnf1o2  6841  exmidpw  7066  exmidpw2en  7070  unfiexmid  7076  xpfi  7090  ssfirab  7094  fnfi  7099  iunfidisj  7109  fidcenumlemr  7118  sbthlemi10  7129  ctmlemr  7271  nninfex  7284  exmidonfinlem  7367  acfun  7385  exmidaclem  7386  pw1ne1  7410  ccfunen  7446  nqex  7546  nq0ex  7623  1pr  7737  ltexprlempr  7791  recexprlempr  7815  cauappcvgprlemcl  7836  caucvgprlemcl  7859  caucvgprprlemcl  7887  addvalex  8027  peano1nnnn  8035  peano2nnnn  8036  axcnex  8042  ax1cn  8044  ax1re  8045  pnfxr  8195  mnfxr  8199  inelr  8727  cju  9104  2re  9176  3re  9180  4re  9183  5re  9185  6re  9187  7re  9189  8re  9191  9re  9193  2nn  9268  3nn  9269  4nn  9270  5nn  9271  6nn  9272  7nn  9273  8nn  9274  9nn  9275  nn0ex  9371  nneoor  9545  zeo  9548  deccl  9588  decnncl  9593  numnncl2  9596  decnncl2  9597  numsucc  9613  numma2c  9619  numadd  9620  numaddc  9621  nummul1c  9622  nummul2c  9623  xnegcl  10024  xrex  10048  ioof  10163  uzennn  10653  xnn0nnen  10654  seqex  10666  m1expcl2  10778  faccl  10952  facwordi  10957  faclbnd2  10959  bccl  10984  lswex  11118  crre  11363  remim  11366  absval  11507  climle  11840  climcvg1nlem  11855  iserabs  11981  geo2lim  12022  prodfclim1  12050  fprodle  12146  ere  12176  ege2le3  12177  eftlub  12196  efsep  12197  tan0  12237  ef01bndlem  12262  nn0o  12413  pczpre  12815  pockthi  12876  igz  12892  ennnfonelemj0  12967  ennnfonelem0  12971  ndxarg  13050  ndxslid  13052  strndxid  13055  basendxnn  13083  strle1g  13134  plusgndxnn  13139  2strbasg  13148  2stropg  13149  tsetndxnn  13217  plendxnn  13231  dsndxnn  13246  unifndxnn  13256  rmodislmodlem  14308  rmodislmod  14309  cndsex  14511  znval  14594  znle  14595  znbaslemnn  14597  znbas  14602  znzrhval  14605  psrval  14624  fczpsrbag  14629  setsmsbasg  15147  cnbl0  15202  cnopncntop  15212  cnopn  15213  remet  15216  divcnap  15233  expcn  15237  climcncf  15252  idcncf  15269  expcncf  15277  cnrehmeocntop  15278  hovercncf  15314  plyrecj  15431  sincn  15437  coscn  15438  2logb9irrALT  15642  2irrexpq  15644  2irrexpqap  15646  lgslem4  15676  lgsdir2lem2  15702  edgfndxnn  15803  setsvtx  15846  usgrstrrepeen  16023  bdinex2  16221  bj-inex  16228  012of  16316  2o01f  16317  peano3nninf  16332  cvgcmp2nlemabs  16359  trilpolemisumle  16365