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  6663  frecex  6670  1on  6699  2on  6701  3on  6703  4on  6705  2oex  6709  1onn  6798  2onn  6799  3onn  6800  4onn  6801  mapsnf1o2  6984  exmidpw  7221  exmidpw2en  7225  unfiexmid  7231  xpfi  7245  ssfirab  7250  fnfi  7256  iunfidisj  7266  fidcenumlemr  7279  sbthlemi10  7290  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  9758  zeo  9761  deccl  9801  decnncl  9810  numnncl2  9814  decnncl2  9815  numsucc  9831  numma2c  9837  numadd  9838  numaddc  9839  nummul1c  9840  nummul2c  9841  xnegcl  10250  xrex  10274  ioof  10389  uzennn  10893  xnn0nnen  10894  seqex  10906  m1expcl2  11018  faccl  11194  facwordi  11199  faclbnd2  11201  bccl  11226  hashf1lem2  11307  lswex  11377  crre  11643  remim  11646  absval  11788  climle  12124  climcvg1nlem  12139  iserabs  12266  geo2lim  12307  prodfclim1  12335  fprodle  12431  ere  12461  ege2le3  12462  eftlub  12481  efsep  12482  tan0  12522  ef01bndlem  12547  nn0o  12698  pczpre  13104  pockthi  13165  igz  13181  1259lem1  13270  1259lem2  13271  1259lem3  13272  1259lem4  13273  1259lem5  13274  1259prm  13275  ballotfilemofi  13276  ballotfilemonn  13278  ballotfilemefi  13294  ballotfilem7  13336  ennnfonelemj0  13349  ennnfonelem0  13353  ndxarg  13432  ndxslid  13434  strndxid  13437  basendxnn  13465  strle1g  13518  plusgndxnn  13523  2strbasg  13532  2stropg  13533  tsetndxnn  13601  plendxnn  13615  dsndxnn  13630  unifndxnn  13640  rmodislmodlem  14795  rmodislmod  14796  cndsex  14998  znval  15079  znle  15080  znbaslemnn  15082  znbas  15087  znzrhval  15090  psrval  15160  fczpsrbag  15169  setsmsbasg  15722  cnbl0  15777  cnopncntop  15787  cnopn  15788  remet  15791  divcnap  15808  expcn  15812  climcncf  15827  idcncf  15844  expcncf  15852  cnrehmeocntop  15853  hovercncf  15889  plyrecj  16006  sincn  16012  coscn  16013  2logb9irrALT  16227  2irrexpq  16229  2irrexpqap  16231  birthdaylog2  16245  ppiublem1  16308  bposlem6  16333  bposlem8  16335  lgslem4  16344  lgsdir2lem2  16370  edgfndxnn  16471  setsvtx  16514  usgrstrrepeen  16694  eulerpathprum  16943  konigsbergumgr  16950  konigsberglem5  16955  konigsberg  16956  bdinex2  17148  bj-inex  17155  012of  17245  2o01f  17246  peano3nninf  17273  cvgcmp2nlemabs  17304  trilpolemisumle  17311