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  7449  nninfex  7462  exmidonfinlem  7546  acfun  7564  exmidaclem  7565  pw1ne1  7589  ccfunen  7631  nqex  7731  nq0ex  7808  1pr  7922  ltexprlempr  7976  recexprlempr  8000  cauappcvgprlemcl  8021  caucvgprlemcl  8044  caucvgprprlemcl  8072  addvalex  8212  peano1nnnn  8220  peano2nnnn  8221  axcnex  8227  ax1cn  8229  ax1re  8230  pnfxr  8379  mnfxr  8383  inelr  8915  cju  9294  2re  9377  3re  9381  4re  9384  5re  9386  6re  9388  7re  9390  8re  9392  9re  9394  2nn  9471  3nn  9472  4nn  9473  5nn  9474  6nn  9475  7nn  9476  8nn  9477  9nn  9478  nn0ex  9574  nneoor  9753  zeo  9756  deccl  9796  decnncl  9805  numnncl2  9809  decnncl2  9810  numsucc  9826  numma2c  9832  numadd  9833  numaddc  9834  nummul1c  9835  nummul2c  9836  xnegcl  10245  xrex  10269  ioof  10384  uzennn  10888  xnn0nnen  10889  seqex  10901  m1expcl2  11013  faccl  11189  facwordi  11194  faclbnd2  11196  bccl  11221  hashf1lem2  11302  lswex  11372  crre  11638  remim  11641  absval  11783  climle  12119  climcvg1nlem  12134  iserabs  12261  geo2lim  12302  prodfclim1  12330  fprodle  12426  ere  12456  ege2le3  12457  eftlub  12476  efsep  12477  tan0  12517  ef01bndlem  12542  nn0o  12693  pczpre  13099  pockthi  13160  igz  13176  1259lem1  13265  1259lem2  13266  1259lem3  13267  1259lem4  13268  1259lem5  13269  1259prm  13270  ballotfilemofi  13271  ballotfilemonn  13273  ballotfilemefi  13289  ballotfilem7  13331  ennnfonelemj0  13344  ennnfonelem0  13348  ndxarg  13427  ndxslid  13429  strndxid  13432  basendxnn  13460  strle1g  13513  plusgndxnn  13518  2strbasg  13527  2stropg  13528  tsetndxnn  13596  plendxnn  13610  dsndxnn  13625  unifndxnn  13635  rmodislmodlem  14778  rmodislmod  14779  cndsex  14981  znval  15062  znle  15063  znbaslemnn  15065  znbas  15070  znzrhval  15073  psrval  15141  fczpsrbag  15147  setsmsbasg  15679  cnbl0  15734  cnopncntop  15744  cnopn  15745  remet  15748  divcnap  15765  expcn  15769  climcncf  15784  idcncf  15801  expcncf  15809  cnrehmeocntop  15810  hovercncf  15846  plyrecj  15963  sincn  15969  coscn  15970  2logb9irrALT  16184  2irrexpq  16186  2irrexpqap  16188  birthdaylog2  16202  ppiublem1  16265  bposlem6  16290  bposlem8  16292  lgslem4  16301  lgsdir2lem2  16327  edgfndxnn  16428  setsvtx  16471  usgrstrrepeen  16651  eulerpathprum  16900  konigsbergumgr  16907  konigsberglem5  16912  konigsberg  16913  bdinex2  17105  bj-inex  17112  012of  17202  2o01f  17203  peano3nninf  17229  cvgcmp2nlemabs  17260  trilpolemisumle  17267