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

Syntax hints:   = wceq 1402   e. wcel 2209

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

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

This theorem is referenced by:  eqeltrri  2312  3eltr4i  2320  intab  3997  inex2  4266  vpwex  4314  ord3ex  4325  vsnex  4346  uniopel  4395  onsucelsucexmid  4675  nnpredcl  4768  elvvuni  4837  isarep2  5466  acexmidlemcase  6073  abrexex2  6346  oprabex  6354  oprabrexex2  6356  mpoexw  6442  rdg0  6651  frecex  6658  1on  6687  2on  6689  3on  6691  4on  6693  2oex  6697  1onn  6786  2onn  6787  3onn  6788  4onn  6789  mapsnf1o2  6971  exmidpw  7208  exmidpw2en  7212  unfiexmid  7218  xpfi  7232  ssfirab  7237  fnfi  7243  iunfidisj  7253  fidcenumlemr  7265  sbthlemi10  7276  fczfsuppd  7290  ctmlemr  7441  nninfex  7454  exmidonfinlem  7538  acfun  7556  exmidaclem  7557  pw1ne1  7581  ccfunen  7623  nqex  7723  nq0ex  7800  1pr  7914  ltexprlempr  7968  recexprlempr  7992  cauappcvgprlemcl  8013  caucvgprlemcl  8036  caucvgprprlemcl  8064  addvalex  8204  peano1nnnn  8212  peano2nnnn  8213  axcnex  8219  ax1cn  8221  ax1re  8222  pnfxr  8371  mnfxr  8375  inelr  8905  cju  9284  2re  9356  3re  9360  4re  9363  5re  9365  6re  9367  7re  9369  8re  9371  9re  9373  2nn  9448  3nn  9449  4nn  9450  5nn  9451  6nn  9452  7nn  9453  8nn  9454  9nn  9455  nn0ex  9551  nneoor  9730  zeo  9733  deccl  9773  decnncl  9778  numnncl2  9781  decnncl2  9782  numsucc  9798  numma2c  9804  numadd  9805  numaddc  9806  nummul1c  9807  nummul2c  9808  xnegcl  10216  xrex  10240  ioof  10355  uzennn  10854  xnn0nnen  10855  seqex  10867  m1expcl2  10979  faccl  11154  facwordi  11159  faclbnd2  11161  bccl  11186  hashf1lem2  11267  lswex  11337  crre  11603  remim  11606  absval  11748  climle  12081  climcvg1nlem  12096  iserabs  12223  geo2lim  12264  prodfclim1  12292  fprodle  12388  ere  12418  ege2le3  12419  eftlub  12438  efsep  12439  tan0  12479  ef01bndlem  12504  nn0o  12655  pczpre  13057  pockthi  13118  igz  13134  ballotfilemofi  13200  ballotfilemonn  13202  ballotfilemefi  13218  ballotfilem7  13260  ennnfonelemj0  13273  ennnfonelem0  13277  ndxarg  13356  ndxslid  13358  strndxid  13361  basendxnn  13389  strle1g  13440  plusgndxnn  13445  2strbasg  13454  2stropg  13455  tsetndxnn  13523  plendxnn  13537  dsndxnn  13552  unifndxnn  13562  rmodislmodlem  14662  rmodislmod  14663  cndsex  14865  znval  14946  znle  14947  znbaslemnn  14949  znbas  14954  znzrhval  14957  psrval  14976  fczpsrbag  14982  setsmsbasg  15506  cnbl0  15561  cnopncntop  15571  cnopn  15572  remet  15575  divcnap  15592  expcn  15596  climcncf  15611  idcncf  15628  expcncf  15636  cnrehmeocntop  15637  hovercncf  15673  plyrecj  15790  sincn  15796  coscn  15797  2logb9irrALT  16002  2irrexpq  16004  2irrexpqap  16006  lgslem4  16039  lgsdir2lem2  16065  edgfndxnn  16166  setsvtx  16209  usgrstrrepeen  16389  eulerpathprum  16638  konigsbergumgr  16645  konigsberglem5  16650  konigsberg  16651  bdinex2  16843  bj-inex  16850  012of  16940  2o01f  16941  peano3nninf  16958  cvgcmp2nlemabs  16989  trilpolemisumle  16995