Theorem eqeltri 2302

Description: Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
eqeltr.1	|- A = B
eqeltr.2	|- B e. C

Assertion

Ref	Expression
eqeltri	|- A e. C

Proof of Theorem eqeltri

Step	Hyp	Ref	Expression
1		eqeltr.2	. 2 |- B e. C
2		eqeltr.1	. . 3 |- A = B
3	2	eleq1i 2295	. 2 |- ( A e. C <-> B e. C )
4	1, 3	mpbir 146	1 |- A e. C

Syntax hints:   = wceq 1395   e. 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  4264  ord3ex  4275  uniopel  4344  onsucelsucexmid  4623  nnpredcl  4716  elvvuni  4785  isarep2  5411  acexmidlemcase  6005  abrexex2  6278  oprabex  6282  oprabrexex2  6284  mpoexw  6370  rdg0  6544  frecex  6551  1on  6580  2on  6582  3on  6584  4on  6586  2oex  6590  1onn  6679  2onn  6680  3onn  6681  4onn  6682  mapsnf1o2  6856  exmidpw  7086  exmidpw2en  7090  unfiexmid  7096  xpfi  7110  ssfirab  7114  fnfi  7119  iunfidisj  7129  fidcenumlemr  7138  sbthlemi10  7149  ctmlemr  7291  nninfex  7304  exmidonfinlem  7387  acfun  7405  exmidaclem  7406  pw1ne1  7430  ccfunen  7466  nqex  7566  nq0ex  7643  1pr  7757  ltexprlempr  7811  recexprlempr  7835  cauappcvgprlemcl  7856  caucvgprlemcl  7879  caucvgprprlemcl  7907  addvalex  8047  peano1nnnn  8055  peano2nnnn  8056  axcnex  8062  ax1cn  8064  ax1re  8065  pnfxr  8215  mnfxr  8219  inelr  8747  cju  9124  2re  9196  3re  9200  4re  9203  5re  9205  6re  9207  7re  9209  8re  9211  9re  9213  2nn  9288  3nn  9289  4nn  9290  5nn  9291  6nn  9292  7nn  9293  8nn  9294  9nn  9295  nn0ex  9391  nneoor  9565  zeo  9568  deccl  9608  decnncl  9613  numnncl2  9616  decnncl2  9617  numsucc  9633  numma2c  9639  numadd  9640  numaddc  9641  nummul1c  9642  nummul2c  9643  xnegcl  10045  xrex  10069  ioof  10184  uzennn  10675  xnn0nnen  10676  seqex  10688  m1expcl2  10800  faccl  10974  facwordi  10979  faclbnd2  10981  bccl  11006  lswex  11141  crre  11389  remim  11392  absval  11533  climle  11866  climcvg1nlem  11881  iserabs  12007  geo2lim  12048  prodfclim1  12076  fprodle  12172  ere  12202  ege2le3  12203  eftlub  12222  efsep  12223  tan0  12263  ef01bndlem  12288  nn0o  12439  pczpre  12841  pockthi  12902  igz  12918  ennnfonelemj0  12993  ennnfonelem0  12997  ndxarg  13076  ndxslid  13078  strndxid  13081  basendxnn  13109  strle1g  13160  plusgndxnn  13165  2strbasg  13174  2stropg  13175  tsetndxnn  13243  plendxnn  13257  dsndxnn  13272  unifndxnn  13282  rmodislmodlem  14335  rmodislmod  14336  cndsex  14538  znval  14621  znle  14622  znbaslemnn  14624  znbas  14629  znzrhval  14632  psrval  14651  fczpsrbag  14656  setsmsbasg  15174  cnbl0  15229  cnopncntop  15239  cnopn  15240  remet  15243  divcnap  15260  expcn  15264  climcncf  15279  idcncf  15296  expcncf  15304  cnrehmeocntop  15305  hovercncf  15341  plyrecj  15458  sincn  15464  coscn  15465  2logb9irrALT  15669  2irrexpq  15671  2irrexpqap  15673  lgslem4  15703  lgsdir2lem2  15729  edgfndxnn  15830  setsvtx  15873  usgrstrrepeen  16050  bdinex2  16372  bj-inex  16379  012of  16470  2o01f  16471  peano3nninf  16487  cvgcmp2nlemabs  16514  trilpolemisumle  16520