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  3952  inex2  4219  vpwex  4263  ord3ex  4274  uniopel  4343  onsucelsucexmid  4622  nnpredcl  4715  elvvuni  4783  isarep2  5408  acexmidlemcase  6002  abrexex2  6275  oprabex  6279  oprabrexex2  6281  mpoexw  6365  rdg0  6539  frecex  6546  1on  6575  2on  6577  3on  6579  4on  6581  2oex  6585  1onn  6674  2onn  6675  3onn  6676  4onn  6677  mapsnf1o2  6851  exmidpw  7081  exmidpw2en  7085  unfiexmid  7091  xpfi  7105  ssfirab  7109  fnfi  7114  iunfidisj  7124  fidcenumlemr  7133  sbthlemi10  7144  ctmlemr  7286  nninfex  7299  exmidonfinlem  7382  acfun  7400  exmidaclem  7401  pw1ne1  7425  ccfunen  7461  nqex  7561  nq0ex  7638  1pr  7752  ltexprlempr  7806  recexprlempr  7830  cauappcvgprlemcl  7851  caucvgprlemcl  7874  caucvgprprlemcl  7902  addvalex  8042  peano1nnnn  8050  peano2nnnn  8051  axcnex  8057  ax1cn  8059  ax1re  8060  pnfxr  8210  mnfxr  8214  inelr  8742  cju  9119  2re  9191  3re  9195  4re  9198  5re  9200  6re  9202  7re  9204  8re  9206  9re  9208  2nn  9283  3nn  9284  4nn  9285  5nn  9286  6nn  9287  7nn  9288  8nn  9289  9nn  9290  nn0ex  9386  nneoor  9560  zeo  9563  deccl  9603  decnncl  9608  numnncl2  9611  decnncl2  9612  numsucc  9628  numma2c  9634  numadd  9635  numaddc  9636  nummul1c  9637  nummul2c  9638  xnegcl  10040  xrex  10064  ioof  10179  uzennn  10670  xnn0nnen  10671  seqex  10683  m1expcl2  10795  faccl  10969  facwordi  10974  faclbnd2  10976  bccl  11001  lswex  11136  crre  11383  remim  11386  absval  11527  climle  11860  climcvg1nlem  11875  iserabs  12001  geo2lim  12042  prodfclim1  12070  fprodle  12166  ere  12196  ege2le3  12197  eftlub  12216  efsep  12217  tan0  12257  ef01bndlem  12282  nn0o  12433  pczpre  12835  pockthi  12896  igz  12912  ennnfonelemj0  12987  ennnfonelem0  12991  ndxarg  13070  ndxslid  13072  strndxid  13075  basendxnn  13103  strle1g  13154  plusgndxnn  13159  2strbasg  13168  2stropg  13169  tsetndxnn  13237  plendxnn  13251  dsndxnn  13266  unifndxnn  13276  rmodislmodlem  14329  rmodislmod  14330  cndsex  14532  znval  14615  znle  14616  znbaslemnn  14618  znbas  14623  znzrhval  14626  psrval  14645  fczpsrbag  14650  setsmsbasg  15168  cnbl0  15223  cnopncntop  15233  cnopn  15234  remet  15237  divcnap  15254  expcn  15258  climcncf  15273  idcncf  15290  expcncf  15298  cnrehmeocntop  15299  hovercncf  15335  plyrecj  15452  sincn  15458  coscn  15459  2logb9irrALT  15663  2irrexpq  15665  2irrexpqap  15667  lgslem4  15697  lgsdir2lem2  15723  edgfndxnn  15824  setsvtx  15867  usgrstrrepeen  16044  bdinex2  16318  bj-inex  16325  012of  16416  2o01f  16417  peano3nninf  16433  cvgcmp2nlemabs  16460  trilpolemisumle  16466