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  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  11384  remim  11387  absval  11528  climle  11861  climcvg1nlem  11876  iserabs  12002  geo2lim  12043  prodfclim1  12071  fprodle  12167  ere  12197  ege2le3  12198  eftlub  12217  efsep  12218  tan0  12258  ef01bndlem  12283  nn0o  12434  pczpre  12836  pockthi  12897  igz  12913  ennnfonelemj0  12988  ennnfonelem0  12992  ndxarg  13071  ndxslid  13073  strndxid  13076  basendxnn  13104  strle1g  13155  plusgndxnn  13160  2strbasg  13169  2stropg  13170  tsetndxnn  13238  plendxnn  13252  dsndxnn  13267  unifndxnn  13277  rmodislmodlem  14330  rmodislmod  14331  cndsex  14533  znval  14616  znle  14617  znbaslemnn  14619  znbas  14624  znzrhval  14627  psrval  14646  fczpsrbag  14651  setsmsbasg  15169  cnbl0  15224  cnopncntop  15234  cnopn  15235  remet  15238  divcnap  15255  expcn  15259  climcncf  15274  idcncf  15291  expcncf  15299  cnrehmeocntop  15300  hovercncf  15336  plyrecj  15453  sincn  15459  coscn  15460  2logb9irrALT  15664  2irrexpq  15666  2irrexpqap  15668  lgslem4  15698  lgsdir2lem2  15724  edgfndxnn  15825  setsvtx  15868  usgrstrrepeen  16045  bdinex2  16346  bj-inex  16353  012of  16444  2o01f  16445  peano3nninf  16461  cvgcmp2nlemabs  16488  trilpolemisumle  16494