Theorem eqeltri 2307

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 2300	. 2 |- ( A e. C <-> B e. C )
4	1, 3	mpbir 146	1 |- A e. C

Syntax hints:   = wceq 1398   e. wcel 2205

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-clel 2230

This theorem is referenced by:  eqeltrri  2308  3eltr4i  2316  intab  3980  inex2  4247  vpwex  4294  ord3ex  4305  vsnex  4326  uniopel  4375  onsucelsucexmid  4654  nnpredcl  4747  elvvuni  4816  isarep2  5445  acexmidlemcase  6047  abrexex2  6319  oprabex  6323  oprabrexex2  6325  mpoexw  6411  rdg0  6620  frecex  6627  1on  6656  2on  6658  3on  6660  4on  6662  2oex  6666  1onn  6755  2onn  6756  3onn  6757  4onn  6758  mapsnf1o2  6933  exmidpw  7170  exmidpw2en  7174  unfiexmid  7180  xpfi  7194  ssfirab  7199  fnfi  7205  iunfidisj  7215  fidcenumlemr  7227  sbthlemi10  7238  fczfsuppd  7252  ctmlemr  7401  nninfex  7414  exmidonfinlem  7498  acfun  7516  exmidaclem  7517  pw1ne1  7541  ccfunen  7580  nqex  7680  nq0ex  7757  1pr  7871  ltexprlempr  7925  recexprlempr  7949  cauappcvgprlemcl  7970  caucvgprlemcl  7993  caucvgprprlemcl  8021  addvalex  8161  peano1nnnn  8169  peano2nnnn  8170  axcnex  8176  ax1cn  8178  ax1re  8179  pnfxr  8328  mnfxr  8332  inelr  8860  cju  9237  2re  9309  3re  9313  4re  9316  5re  9318  6re  9320  7re  9322  8re  9324  9re  9326  2nn  9401  3nn  9402  4nn  9403  5nn  9404  6nn  9405  7nn  9406  8nn  9407  9nn  9408  nn0ex  9504  nneoor  9683  zeo  9686  deccl  9726  decnncl  9731  numnncl2  9734  decnncl2  9735  numsucc  9751  numma2c  9757  numadd  9758  numaddc  9759  nummul1c  9760  nummul2c  9761  xnegcl  10168  xrex  10192  ioof  10307  uzennn  10802  xnn0nnen  10803  seqex  10815  m1expcl2  10927  faccl  11101  facwordi  11106  faclbnd2  11108  bccl  11133  lswex  11280  crre  11546  remim  11549  absval  11690  climle  12023  climcvg1nlem  12038  iserabs  12165  geo2lim  12206  prodfclim1  12234  fprodle  12330  ere  12360  ege2le3  12361  eftlub  12380  efsep  12381  tan0  12421  ef01bndlem  12446  nn0o  12597  pczpre  12999  pockthi  13060  igz  13076  ballotfilemofi  13142  ballotfilemonn  13144  ennnfonelemj0  13169  ennnfonelem0  13173  ndxarg  13252  ndxslid  13254  strndxid  13257  basendxnn  13285  strle1g  13336  plusgndxnn  13341  2strbasg  13350  2stropg  13351  tsetndxnn  13419  plendxnn  13433  dsndxnn  13448  unifndxnn  13458  rmodislmodlem  14515  rmodislmod  14516  cndsex  14718  znval  14801  znle  14802  znbaslemnn  14804  znbas  14809  znzrhval  14812  psrval  14831  fczpsrbag  14837  setsmsbasg  15361  cnbl0  15416  cnopncntop  15426  cnopn  15427  remet  15430  divcnap  15447  expcn  15451  climcncf  15466  idcncf  15483  expcncf  15491  cnrehmeocntop  15492  hovercncf  15528  plyrecj  15645  sincn  15651  coscn  15652  2logb9irrALT  15856  2irrexpq  15858  2irrexpqap  15860  lgslem4  15893  lgsdir2lem2  15919  edgfndxnn  16020  setsvtx  16063  usgrstrrepeen  16243  eulerpathprum  16492  konigsbergumgr  16499  konigsberglem5  16504  konigsberg  16505  bdinex2  16687  bj-inex  16694  012of  16784  2o01f  16785  peano3nninf  16802  cvgcmp2nlemabs  16833  trilpolemisumle  16839