Theorem eqeltri 2311

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

This proof depends on syntax axioms:   = wceq 1402   e. wcel 2209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  eqeltrri  2312  3eltr4i  2320  intab  3999  inex2  4268  vpwex  4316  ord3ex  4327  vsnex  4348  uniopel  4397  onsucelsucexmid  4677  nnpredcl  4770  elvvuni  4839  isarep2  5468  acexmidlemcase  6080  abrexex2  6353  oprabex  6361  oprabrexex2  6363  mpoexw  6449  rdg0  6658  frecex  6665  1on  6694  2on  6696  3on  6698  4on  6700  2oex  6704  1onn  6793  2onn  6794  3onn  6795  4onn  6796  mapsnf1o2  6978  exmidpw  7215  exmidpw2en  7219  unfiexmid  7225  xpfi  7239  ssfirab  7244  fnfi  7250  iunfidisj  7260  fidcenumlemr  7272  sbthlemi10  7283  fczfsuppd  7297  ctmlemr  7448  nninfex  7461  exmidonfinlem  7545  acfun  7563  exmidaclem  7564  pw1ne1  7588  ccfunen  7630  nqex  7730  nq0ex  7807  1pr  7921  ltexprlempr  7975  recexprlempr  7999  cauappcvgprlemcl  8020  caucvgprlemcl  8043  caucvgprprlemcl  8071  addvalex  8211  peano1nnnn  8219  peano2nnnn  8220  axcnex  8226  ax1cn  8228  ax1re  8229  pnfxr  8378  mnfxr  8382  inelr  8912  cju  9291  2re  9374  3re  9378  4re  9381  5re  9383  6re  9385  7re  9387  8re  9389  9re  9391  2nn  9466  3nn  9467  4nn  9468  5nn  9469  6nn  9470  7nn  9471  8nn  9472  9nn  9473  nn0ex  9569  nneoor  9748  zeo  9751  deccl  9791  decnncl  9796  numnncl2  9799  decnncl2  9800  numsucc  9816  numma2c  9822  numadd  9823  numaddc  9824  nummul1c  9825  nummul2c  9826  xnegcl  10234  xrex  10258  ioof  10373  uzennn  10873  xnn0nnen  10874  seqex  10886  m1expcl2  10998  faccl  11173  facwordi  11178  faclbnd2  11180  bccl  11205  hashf1lem2  11286  lswex  11356  crre  11622  remim  11625  absval  11767  climle  12100  climcvg1nlem  12115  iserabs  12242  geo2lim  12283  prodfclim1  12311  fprodle  12407  ere  12437  ege2le3  12438  eftlub  12457  efsep  12458  tan0  12498  ef01bndlem  12523  nn0o  12674  pczpre  13076  pockthi  13137  igz  13153  ballotfilemofi  13219  ballotfilemonn  13221  ballotfilemefi  13237  ballotfilem7  13279  ennnfonelemj0  13292  ennnfonelem0  13296  ndxarg  13375  ndxslid  13377  strndxid  13380  basendxnn  13408  strle1g  13460  plusgndxnn  13465  2strbasg  13474  2stropg  13475  tsetndxnn  13543  plendxnn  13557  dsndxnn  13572  unifndxnn  13582  rmodislmodlem  14687  rmodislmod  14688  cndsex  14890  znval  14971  znle  14972  znbaslemnn  14974  znbas  14979  znzrhval  14982  psrval  15050  fczpsrbag  15056  setsmsbasg  15580  cnbl0  15635  cnopncntop  15645  cnopn  15646  remet  15649  divcnap  15666  expcn  15670  climcncf  15685  idcncf  15702  expcncf  15710  cnrehmeocntop  15711  hovercncf  15747  plyrecj  15864  sincn  15870  coscn  15871  2logb9irrALT  16076  2irrexpq  16078  2irrexpqap  16080  birthdaylog2  16090  lgslem4  16122  lgsdir2lem2  16148  edgfndxnn  16249  setsvtx  16292  usgrstrrepeen  16472  eulerpathprum  16721  konigsbergumgr  16728  konigsberglem5  16733  konigsberg  16734  bdinex2  16926  bj-inex  16933  012of  17023  2o01f  17024  peano3nninf  17050  cvgcmp2nlemabs  17081  trilpolemisumle  17087