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 ⊢ 𝐴 ∈ 𝐶

Syntax hints:   = wceq 1402   ∈ 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  3994  inex2  4263  vpwex  4311  ord3ex  4322  vsnex  4343  uniopel  4392  onsucelsucexmid  4672  nnpredcl  4765  elvvuni  4834  isarep2  5463  acexmidlemcase  6070  abrexex2  6343  oprabex  6351  oprabrexex2  6353  mpoexw  6439  rdg0  6648  frecex  6655  1on  6684  2on  6686  3on  6688  4on  6690  2oex  6694  1onn  6783  2onn  6784  3onn  6785  4onn  6786  mapsnf1o2  6968  exmidpw  7205  exmidpw2en  7209  unfiexmid  7215  xpfi  7229  ssfirab  7234  fnfi  7240  iunfidisj  7250  fidcenumlemr  7262  sbthlemi10  7273  fczfsuppd  7287  ctmlemr  7438  nninfex  7451  exmidonfinlem  7535  acfun  7553  exmidaclem  7554  pw1ne1  7578  ccfunen  7620  nqex  7720  nq0ex  7797  1pr  7911  ltexprlempr  7965  recexprlempr  7989  cauappcvgprlemcl  8010  caucvgprlemcl  8033  caucvgprprlemcl  8061  addvalex  8201  peano1nnnn  8209  peano2nnnn  8210  axcnex  8216  ax1cn  8218  ax1re  8219  pnfxr  8368  mnfxr  8372  inelr  8902  cju  9281  2re  9353  3re  9357  4re  9360  5re  9362  6re  9364  7re  9366  8re  9368  9re  9370  2nn  9445  3nn  9446  4nn  9447  5nn  9448  6nn  9449  7nn  9450  8nn  9451  9nn  9452  nn0ex  9548  nneoor  9727  zeo  9730  deccl  9770  decnncl  9775  numnncl2  9778  decnncl2  9779  numsucc  9795  numma2c  9801  numadd  9802  numaddc  9803  nummul1c  9804  nummul2c  9805  xnegcl  10213  xrex  10237  ioof  10352  uzennn  10851  xnn0nnen  10852  seqex  10864  m1expcl2  10976  faccl  11151  facwordi  11156  faclbnd2  11158  bccl  11183  hashf1lem2  11264  lswex  11334  crre  11600  remim  11603  absval  11745  climle  12078  climcvg1nlem  12093  iserabs  12220  geo2lim  12261  prodfclim1  12289  fprodle  12385  ere  12415  ege2le3  12416  eftlub  12435  efsep  12436  tan0  12476  ef01bndlem  12501  nn0o  12652  pczpre  13054  pockthi  13115  igz  13131  ballotfilemofi  13197  ballotfilemonn  13199  ballotfilemefi  13215  ballotfilem7  13257  ennnfonelemj0  13270  ennnfonelem0  13274  ndxarg  13353  ndxslid  13355  strndxid  13358  basendxnn  13386  strle1g  13437  plusgndxnn  13442  2strbasg  13451  2stropg  13452  tsetndxnn  13520  plendxnn  13534  dsndxnn  13549  unifndxnn  13559  rmodislmodlem  14659  rmodislmod  14660  cndsex  14862  znval  14943  znle  14944  znbaslemnn  14946  znbas  14951  znzrhval  14954  psrval  14973  fczpsrbag  14979  setsmsbasg  15503  cnbl0  15558  cnopncntop  15568  cnopn  15569  remet  15572  divcnap  15589  expcn  15593  climcncf  15608  idcncf  15625  expcncf  15633  cnrehmeocntop  15634  hovercncf  15670  plyrecj  15787  sincn  15793  coscn  15794  2logb9irrALT  15999  2irrexpq  16001  2irrexpqap  16003  lgslem4  16036  lgsdir2lem2  16062  edgfndxnn  16163  setsvtx  16206  usgrstrrepeen  16386  eulerpathprum  16635  konigsbergumgr  16642  konigsberglem5  16647  konigsberg  16648  bdinex2  16840  bj-inex  16847  012of  16937  2o01f  16938  peano3nninf  16955  cvgcmp2nlemabs  16986  trilpolemisumle  16992