Theorem eqeltrri 2727

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

Hypotheses

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

Assertion

Ref	Expression
eqeltrri	⊢ 𝐵 ∈ 𝐶

Proof of Theorem eqeltrri

Step	Hyp	Ref	Expression
1		eqeltrr.1	. . 3 ⊢ 𝐴 = 𝐵
2	1	eqcomi 2660	. 2 ⊢ 𝐵 = 𝐴
3		eqeltrr.2	. 2 ⊢ 𝐴 ∈ 𝐶
4	2, 3	eqeltri 2726	1 ⊢ 𝐵 ∈ 𝐶

Syntax hints:   = wceq 1523   ∈ wcel 2030

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644  df-clel 2647

This theorem is referenced by:  3eltr3i  2742  zfrep4  4812  p0ex  4883  pp0ex  4885  ord3ex  4886  zfpair  4934  epse  5126  unex  6998  fvresex  7181  abrexexOLD  7184  opabex3  7188  abexssex  7191  abrexex2OLD  7192  abexex  7193  oprabrexex2  7200  seqomlem3  7592  inf0  8556  scottexs  8788  kardex  8795  infxpenlem  8874  r1om  9104  cfon  9115  fin23lem16  9195  fin1a2lem6  9265  hsmexlem5  9290  brdom7disj  9391  brdom6disj  9392  1lt2pi  9765  0cn  10070  resubcli  10381  0reALT  10416  1nn  11069  10nn  11552  numsucc  11587  nummac  11596  unirnioo  12311  ioorebas  12313  fz0to4untppr  12481  om2uzrani  12791  uzrdg0i  12798  hashunlei  13250  cats1fvn  13649  trclubi  13781  4sqlem19  15714  dec2dvds  15814  mod2xnegi  15822  modsubi  15823  gcdi  15824  isstruct2  15914  grppropstr  17486  ltbval  19519  nn0srg  19864  sn0topon  20850  indistop  20854  indisuni  20855  indistps2  20864  indistps2ALT  20866  restbas  21010  leordtval2  21064  iocpnfordt  21067  icomnfordt  21068  iooordt  21069  reordt  21070  dis1stc  21350  ptcmpfi  21664  ustfn  22052  ustn0  22071  retopbas  22611  blssioo  22645  xrtgioo  22656  zcld  22663  cnperf  22670  retopconn  22679  iimulcn  22784  rembl  23354  mbfdm  23440  ismbf  23442  abelthlem9  24239  advlog  24445  advlogexp  24446  cxpcn3  24534  loglesqrt  24544  log2ub  24721  ppi1i  24939  cht2  24943  cht3  24944  bpos1lem  25052  lgslem4  25070  vmadivsum  25216  log2sumbnd  25278  selberg2  25285  selbergr  25302  iscgrg  25452  ishpg  25696  ax5seglem7  25860  fusgrfis  26267  h2hva  27959  h2hsm  27960  h2hnm  27961  norm-ii-i  28122  hhshsslem2  28253  shincli  28349  chincli  28447  lnophdi  28989  imaelshi  29045  rnelshi  29046  bdophdi  29084  dfdec100  29704  dpadd2  29746  dpmul  29749  dpmul4  29750  nn0omnd  29969  nn0archi  29971  lmatfvlem  30009  rmulccn  30102  rrhre  30193  sigaex  30300  br2base  30459  sxbrsigalem3  30462  carsgclctunlem3  30510  sitmcl  30541  rpsqrtcn  30799  hgt750lem  30857  hgt750lem2  30858  afsval  30877  kur14lem7  31320  retopsconn  31357  hfuni  32416  neibastop2lem  32480  onint1  32573  topdifinffinlem  33325  poimirlem9  33548  poimirlem28  33567  poimirlem30  33569  poimirlem32  33571  0mbf  33585  bddiblnc  33610  ftc1cnnc  33614  cncfres  33694  lineset  35342  lautset  35686  pautsetN  35702  tendoset  36364  areaquad  38119  sblpnf  38826  lhe4.4ex1a  38845  fourierdlem62  40703  fourierdlem76  40717  65537prm  41813  11gbo  41988  bgoldbtbndlem1  42018