Theorem eqeltri 2311

Description: Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
eqeltr.1	⊢ 𝐴 = 𝐵
eqeltr.2	⊢ 𝐵 ∈ 𝐶

Assertion

Ref	Expression
eqeltri	⊢ 𝐴 ∈ 𝐶

Proof of Theorem eqeltri

Step	Hyp	Ref	Expression
1		eqeltr.2	. 2 ⊢ 𝐵 ∈ 𝐶
2		eqeltr.1	. . 3 ⊢ 𝐴 = 𝐵
3	2	eleq1i 2304	. 2 ⊢ (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶)
4	1, 3	mpbir 146	1 ⊢ 𝐴 ∈ 𝐶

This proof depends on syntax axioms:   = wceq 1402   ∈ 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  14771  rmodislmod  14772  cndsex  14974  znval  15055  znle  15056  znbaslemnn  15058  znbas  15063  znzrhval  15066  psrval  15134  fczpsrbag  15140  setsmsbasg  15671  cnbl0  15726  cnopncntop  15736  cnopn  15737  remet  15740  divcnap  15757  expcn  15761  climcncf  15776  idcncf  15793  expcncf  15801  cnrehmeocntop  15802  hovercncf  15838  plyrecj  15955  sincn  15961  coscn  15962  2logb9irrALT  16171  2irrexpq  16173  2irrexpqap  16175  birthdaylog2  16189  ppiublem1  16252  bposlem6  16277  bposlem8  16279  lgslem4  16288  lgsdir2lem2  16314  edgfndxnn  16415  setsvtx  16458  usgrstrrepeen  16638  eulerpathprum  16887  konigsbergumgr  16894  konigsberglem5  16899  konigsberg  16900  bdinex2  17092  bj-inex  17099  012of  17189  2o01f  17190  peano3nninf  17216  cvgcmp2nlemabs  17247  trilpolemisumle  17254