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  4270  vpwex  4318  ord3ex  4329  vsnex  4350  uniopel  4399  onsucelsucexmid  4679  nnpredcl  4772  elvvuni  4841  isarep2  5471  acexmidlemcase  6083  abrexex2  6357  oprabex  6365  oprabrexex2  6367  mpoexw  6453  rdg0  6662  frecex  6669  1on  6698  2on  6700  3on  6702  4on  6704  2oex  6708  1onn  6797  2onn  6798  3onn  6799  4onn  6800  mapsnf1o2  6982  exmidpw  7219  exmidpw2en  7223  unfiexmid  7229  xpfi  7243  ssfirab  7248  fnfi  7254  iunfidisj  7264  fidcenumlemr  7277  sbthlemi10  7288  fczfsuppd  7302  ctmlemr  7454  nninfex  7467  exmidonfinlem  7551  acfun  7569  exmidaclem  7570  pw1ne1  7594  ccfunen  7636  nqex  7736  nq0ex  7813  1pr  7927  ltexprlempr  7981  recexprlempr  8005  cauappcvgprlemcl  8026  caucvgprlemcl  8049  caucvgprprlemcl  8077  addvalex  8217  peano1nnnn  8225  peano2nnnn  8226  axcnex  8232  ax1cn  8234  ax1re  8235  pnfxr  8384  mnfxr  8388  inelr  8920  cju  9299  2re  9383  3re  9387  4re  9390  5re  9392  6re  9394  7re  9396  8re  9398  9re  9400  2nn  9477  3nn  9478  4nn  9479  5nn  9480  6nn  9481  7nn  9482  8nn  9483  9nn  9484  nn0ex  9580  nneoor  9759  zeo  9762  deccl  9802  decnncl  9811  numnncl2  9815  decnncl2  9816  numsucc  9832  numma2c  9838  numadd  9839  numaddc  9840  nummul1c  9841  nummul2c  9842  xnegcl  10251  xrex  10275  ioof  10390  uzennn  10894  xnn0nnen  10895  seqex  10907  m1expcl2  11019  faccl  11195  facwordi  11200  faclbnd2  11202  bccl  11227  hashf1lem2  11308  lswex  11378  crre  11644  remim  11647  absval  11789  climle  12125  climcvg1nlem  12140  iserabs  12267  geo2lim  12308  prodfclim1  12336  fprodle  12432  ere  12462  ege2le3  12463  eftlub  12482  efsep  12483  tan0  12523  ef01bndlem  12548  nn0o  12699  pczpre  13105  pockthi  13166  igz  13182  1259lem1  13271  1259lem2  13272  1259lem3  13273  1259lem4  13274  1259lem5  13275  1259prm  13276  ballotfilemofi  13277  ballotfilemonn  13279  ballotfilemefi  13295  ballotfilem7  13337  ennnfonelemj0  13350  ennnfonelem0  13354  ndxarg  13433  ndxslid  13435  strndxid  13438  basendxnn  13466  strle1g  13519  plusgndxnn  13524  2strbasg  13533  2stropg  13534  tsetndxnn  13602  plendxnn  13616  dsndxnn  13631  unifndxnn  13641  rmodislmodlem  14796  rmodislmod  14797  cndsex  14999  znval  15080  znle  15081  znbaslemnn  15083  znbas  15088  znzrhval  15091  psrval  15159  fczpsrbag  15165  setsmsbasg  15705  cnbl0  15760  cnopncntop  15770  cnopn  15771  remet  15774  divcnap  15791  expcn  15795  climcncf  15810  idcncf  15827  expcncf  15835  cnrehmeocntop  15836  hovercncf  15872  plyrecj  15989  sincn  15995  coscn  15996  2logb9irrALT  16210  2irrexpq  16212  2irrexpqap  16214  birthdaylog2  16228  ppiublem1  16291  bposlem6  16316  bposlem8  16318  lgslem4  16327  lgsdir2lem2  16353  edgfndxnn  16454  setsvtx  16497  usgrstrrepeen  16677  eulerpathprum  16926  konigsbergumgr  16933  konigsberglem5  16938  konigsberg  16939  bdinex2  17131  bj-inex  17138  012of  17228  2o01f  17229  peano3nninf  17256  cvgcmp2nlemabs  17287  trilpolemisumle  17294