Theorem eqeltri 2230

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

Syntax hints:   = wceq 1335   ∈ wcel 2128

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-4 1490  ax-17 1506  ax-ial 1514  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-cleq 2150  df-clel 2153

This theorem is referenced by:  eqeltrri  2231  3eltr4i  2239  intab  3836  inex2  4099  vpwex  4139  ord3ex  4150  uniopel  4215  onsucelsucexmid  4487  nnpredcl  4580  elvvuni  4647  isarep2  5254  acexmidlemcase  5813  abrexex2  6066  oprabex  6070  oprabrexex2  6072  rdg0  6328  frecex  6335  1on  6364  2on  6366  3on  6368  4on  6369  1onn  6460  2onn  6461  3onn  6462  4onn  6463  mapsnf1o2  6634  exmidpw  6846  unfiexmid  6855  xpfi  6867  ssfirab  6871  fnfi  6874  iunfidisj  6883  fidcenumlemr  6892  sbthlemi10  6903  ctmlemr  7042  nninfex  7055  exmidonfinlem  7111  acfun  7125  exmidaclem  7126  pw1ne1  7147  ccfunen  7167  nqex  7266  nq0ex  7343  1pr  7457  ltexprlempr  7511  recexprlempr  7535  cauappcvgprlemcl  7556  caucvgprlemcl  7579  caucvgprprlemcl  7607  addvalex  7747  peano1nnnn  7755  peano2nnnn  7756  axcnex  7762  ax1cn  7764  ax1re  7765  pnfxr  7913  mnfxr  7917  inelr  8442  cju  8815  2re  8886  3re  8890  4re  8893  5re  8895  6re  8897  7re  8899  8re  8901  9re  8903  2nn  8977  3nn  8978  4nn  8979  5nn  8980  6nn  8981  7nn  8982  8nn  8983  9nn  8984  nn0ex  9079  nneoor  9249  zeo  9252  deccl  9292  decnncl  9297  numnncl2  9300  decnncl2  9301  numsucc  9317  numma2c  9323  numadd  9324  numaddc  9325  nummul1c  9326  nummul2c  9327  xnegcl  9718  xrex  9742  ioof  9857  uzennn  10317  seqex  10328  m1expcl2  10423  faccl  10591  facwordi  10596  faclbnd2  10598  bccl  10623  crre  10739  remim  10742  absval  10883  climle  11213  climcvg1nlem  11228  iserabs  11354  geo2lim  11395  prodfclim1  11423  fprodle  11519  ere  11549  ege2le3  11550  eftlub  11569  efsep  11570  tan0  11610  ef01bndlem  11635  nn0o  11779  ennnfonelemj0  12102  ennnfonelem0  12106  ndxarg  12173  ndxslid  12175  strndxid  12178  basendxnn  12205  strle1g  12240  2strbasg  12251  2stropg  12252  setsmsbasg  12839  cnbl0  12894  cnopncntop  12897  remet  12900  divcnap  12915  climcncf  12931  expcncf  12952  cnrehmeocntop  12953  sincn  13050  coscn  13051  2logb9irrALT  13251  2irrexpq  13253  2irrexpqap  13255  bdinex2  13435  bj-inex  13442  012of  13528  2o01f  13529  peano3nninf  13541  cvgcmp2nlemabs  13566  trilpolemisumle  13572