Theorem eqeltrri 2910

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

Hypotheses

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

Assertion

Ref	Expression
eqeltrri	⊢ 𝐵 ∈ 𝐶

Proof of Theorem eqeltrri

Step	Hyp	Ref	Expression
1		eqeltrri.1	. . 3 ⊢ 𝐴 = 𝐵
2	1	eqcomi 2830	. 2 ⊢ 𝐵 = 𝐴
3		eqeltrri.2	. 2 ⊢ 𝐴 ∈ 𝐶
4	2, 3	eqeltri 2909	1 ⊢ 𝐵 ∈ 𝐶

Syntax hints:   = wceq 1533   ∈ wcel 2110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814  df-clel 2893

This theorem is referenced by:  3eltr3i  2925  zfrep4  5192  p0ex  5276  pp0ex  5278  ord3ex  5279  zfpair  5313  epse  5532  unex  7463  fvresex  7655  opabex3  7662  abexssex  7665  abexex  7666  oprabrexex2  7673  seqomlem3  8082  inf0  9078  scottexs  9310  kardex  9317  infxpenlem  9433  r1om  9660  cfon  9671  fin23lem16  9751  fin1a2lem6  9821  hsmexlem5  9846  brdom7disj  9947  brdom6disj  9948  1lt2pi  10321  0cn  10627  resubcli  10942  0reALT  10977  1nn  11643  10nn  12108  numsucc  12132  nummac  12137  unirnioo  12831  ioorebas  12833  fz0to4untppr  13004  om2uzrani  13314  uzrdg0i  13321  hashunlei  13780  cats1fvn  14214  trclubi  14350  4sqlem19  16293  dec2dvds  16393  mod2xnegi  16401  modsubi  16402  gcdi  16403  isstruct2  16487  grppropstr  18114  ltbval  20246  nn0srg  20609  sn0topon  21600  indistop  21604  indisuni  21605  indistps2  21614  indistps2ALT  21616  restbas  21760  leordtval2  21814  iocpnfordt  21817  icomnfordt  21818  iooordt  21819  reordt  21820  dis1stc  22101  ptcmpfi  22415  ustfn  22804  ustn0  22823  retopbas  23363  blssioo  23397  xrtgioo  23408  zcld  23415  cnperf  23422  retopconn  23431  iimulcn  23536  rembl  24135  mbfdm  24221  ismbf  24223  mbf0  24229  abelthlem9  25022  advlog  25231  advlogexp  25232  2irrexpq  25307  cxpcn3  25323  loglesqrt  25333  log2ub  25521  ppi1i  25739  cht2  25743  cht3  25744  bpos1lem  25852  lgslem4  25870  vmadivsum  26052  log2sumbnd  26114  selberg2  26121  selbergr  26138  iscgrg  26292  ishpg  26539  ax5seglem7  26715  h2hva  28745  h2hsm  28746  h2hnm  28747  norm-ii-i  28908  hhshsslem2  29039  shincli  29133  chincli  29231  lnophdi  29773  imaelshi  29829  rnelshi  29830  bdophdi  29868  dfdec100  30541  dpadd2  30581  dpmul  30584  dpmul4  30585  nn0omnd  30909  nn0archi  30911  ccfldextrr  31033  lmatfvlem  31075  rmulccn  31166  rrhre  31257  sigaex  31364  br2base  31522  sxbrsigalem3  31525  carsgclctunlem3  31573  sitmcl  31604  rpsqrtcn  31859  hgt750lem  31917  hgt750lem2  31918  afsval  31937  kur14lem7  32454  retopsconn  32491  satfvsuclem1  32601  fmlasuc0  32626  hfuni  33640  neibastop2lem  33703  onint1  33792  topdifinffinlem  34622  poimirlem9  34895  poimirlem28  34914  poimirlem30  34916  poimirlem32  34918  bddiblnc  34956  ftc1cnnc  34960  cncfres  35037  lineset  36868  lautset  37212  pautsetN  37228  tendoset  37889  decpmulnc  39166  decpmul  39167  areaquad  39816  sblpnf  40635  lhe4.4ex1a  40654  fourierdlem62  42447  fourierdlem76  42461  65537prm  43732  11gbo  43934  bgoldbtbndlem1  43964