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  7448  nninfex  7461  exmidonfinlem  7545  acfun  7563  exmidaclem  7564  pw1ne1  7588  ccfunen  7630  nqex  7730  nq0ex  7807  1pr  7921  ltexprlempr  7975  recexprlempr  7999  cauappcvgprlemcl  8020  caucvgprlemcl  8043  caucvgprprlemcl  8071  addvalex  8211  peano1nnnn  8219  peano2nnnn  8220  axcnex  8226  ax1cn  8228  ax1re  8229  pnfxr  8378  mnfxr  8382  inelr  8914  cju  9293  2re  9376  3re  9380  4re  9383  5re  9385  6re  9387  7re  9389  8re  9391  9re  9393  2nn  9470  3nn  9471  4nn  9472  5nn  9473  6nn  9474  7nn  9475  8nn  9476  9nn  9477  nn0ex  9573  nneoor  9752  zeo  9755  deccl  9795  decnncl  9804  numnncl2  9808  decnncl2  9809  numsucc  9825  numma2c  9831  numadd  9832  numaddc  9833  nummul1c  9834  nummul2c  9835  xnegcl  10244  xrex  10268  ioof  10383  uzennn  10886  xnn0nnen  10887  seqex  10899  m1expcl2  11011  faccl  11187  facwordi  11192  faclbnd2  11194  bccl  11219  hashf1lem2  11300  lswex  11370  crre  11636  remim  11639  absval  11781  climle  12116  climcvg1nlem  12131  iserabs  12258  geo2lim  12299  prodfclim1  12327  fprodle  12423  ere  12453  ege2le3  12454  eftlub  12473  efsep  12474  tan0  12514  ef01bndlem  12539  nn0o  12690  pczpre  13096  pockthi  13157  igz  13173  1259lem1  13262  1259lem2  13263  1259lem3  13264  1259lem4  13265  1259lem5  13266  1259prm  13267  ballotfilemofi  13268  ballotfilemonn  13270  ballotfilemefi  13286  ballotfilem7  13328  ennnfonelemj0  13341  ennnfonelem0  13345  ndxarg  13424  ndxslid  13426  strndxid  13429  basendxnn  13457  strle1g  13509  plusgndxnn  13514  2strbasg  13523  2stropg  13524  tsetndxnn  13592  plendxnn  13606  dsndxnn  13621  unifndxnn  13631  rmodislmodlem  14736  rmodislmod  14737  cndsex  14939  znval  15020  znle  15021  znbaslemnn  15023  znbas  15028  znzrhval  15031  psrval  15099  fczpsrbag  15105  setsmsbasg  15629  cnbl0  15684  cnopncntop  15694  cnopn  15695  remet  15698  divcnap  15715  expcn  15719  climcncf  15734  idcncf  15751  expcncf  15759  cnrehmeocntop  15760  hovercncf  15796  plyrecj  15913  sincn  15919  coscn  15920  2logb9irrALT  16129  2irrexpq  16131  2irrexpqap  16133  birthdaylog2  16147  ppiublem1  16192  lgslem4  16220  lgsdir2lem2  16246  edgfndxnn  16347  setsvtx  16390  usgrstrrepeen  16570  eulerpathprum  16819  konigsbergumgr  16826  konigsberglem5  16831  konigsberg  16832  bdinex2  17024  bj-inex  17031  012of  17121  2o01f  17122  peano3nninf  17148  cvgcmp2nlemabs  17179  trilpolemisumle  17185