Theorem eqeltri 2250

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

Syntax hints:   = wceq 1353   e. wcel 2148

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173

This theorem is referenced by:  eqeltrri  2251  3eltr4i  2259  intab  3872  inex2  4136  vpwex  4177  ord3ex  4188  uniopel  4254  onsucelsucexmid  4527  nnpredcl  4620  elvvuni  4688  isarep2  5300  acexmidlemcase  5865  abrexex2  6120  oprabex  6124  oprabrexex2  6126  mpoexw  6209  rdg0  6383  frecex  6390  1on  6419  2on  6421  3on  6423  4on  6424  1onn  6516  2onn  6517  3onn  6518  4onn  6519  mapsnf1o2  6691  exmidpw  6903  unfiexmid  6912  xpfi  6924  ssfirab  6928  fnfi  6931  iunfidisj  6940  fidcenumlemr  6949  sbthlemi10  6960  ctmlemr  7102  nninfex  7115  exmidonfinlem  7187  acfun  7201  exmidaclem  7202  pw1ne1  7223  ccfunen  7258  nqex  7357  nq0ex  7434  1pr  7548  ltexprlempr  7602  recexprlempr  7626  cauappcvgprlemcl  7647  caucvgprlemcl  7670  caucvgprprlemcl  7698  addvalex  7838  peano1nnnn  7846  peano2nnnn  7847  axcnex  7853  ax1cn  7855  ax1re  7856  pnfxr  8004  mnfxr  8008  inelr  8535  cju  8912  2re  8983  3re  8987  4re  8990  5re  8992  6re  8994  7re  8996  8re  8998  9re  9000  2nn  9074  3nn  9075  4nn  9076  5nn  9077  6nn  9078  7nn  9079  8nn  9080  9nn  9081  nn0ex  9176  nneoor  9349  zeo  9352  deccl  9392  decnncl  9397  numnncl2  9400  decnncl2  9401  numsucc  9417  numma2c  9423  numadd  9424  numaddc  9425  nummul1c  9426  nummul2c  9427  xnegcl  9826  xrex  9850  ioof  9965  uzennn  10429  seqex  10440  m1expcl2  10535  faccl  10706  facwordi  10711  faclbnd2  10713  bccl  10738  crre  10857  remim  10860  absval  11001  climle  11333  climcvg1nlem  11348  iserabs  11474  geo2lim  11515  prodfclim1  11543  fprodle  11639  ere  11669  ege2le3  11670  eftlub  11689  efsep  11690  tan0  11730  ef01bndlem  11755  nn0o  11902  pczpre  12287  pockthi  12346  igz  12362  ennnfonelemj0  12392  ennnfonelem0  12396  ndxarg  12475  ndxslid  12477  strndxid  12480  basendxnn  12508  strle1g  12555  plusgndxnn  12560  2strbasg  12568  2stropg  12569  tsetndxnn  12634  plendxnn  12648  dsndxnn  12659  unifndxnn  12669  setsmsbasg  13761  cnbl0  13816  cnopncntop  13819  remet  13822  divcnap  13837  climcncf  13853  expcncf  13874  cnrehmeocntop  13875  sincn  13972  coscn  13973  2logb9irrALT  14174  2irrexpq  14176  2irrexpqap  14178  lgslem4  14186  lgsdir2lem2  14212  bdinex2  14423  bj-inex  14430  012of  14516  2o01f  14517  peano3nninf  14527  cvgcmp2nlemabs  14551  trilpolemisumle  14557