Theorem eqeltrri 2860

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 2772	. 2 ⊢ 𝐵 = 𝐴
3		eqeltrri.2	. 2 ⊢ 𝐴 ∈ 𝐶
4	2, 3	eqeltri 2859	1 ⊢ 𝐵 ∈ 𝐶

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2143

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-clel 2838

This theorem is used by:  3eltr3i  2875  zfrep4  5254  p0ex  5355  pp0ex  5357  ord3ex  5358  zfpair  5392  moabex  5439  epse  5643  fvresex  7953  opabex3  7960  abexssex  7963  abexex  7964  oprabrexex2  7971  seqomlem3  8435  1on  8462  2on  8463  inf0  9586  scottexsOLD  9868  kardexOLD  9883  infxpenlem  10002  r1om  10231  cfonOLD  10243  fin23lem16  10323  fin1a2lem6  10393  hsmexlem5  10418  brdom7disj  10519  brdom6disj  10520  1lt2pi  10894  0cn  11202  resubcli  11524  0reALT  11559  1nn  12248  10nn  12735  numsucc  12760  nummac  12765  unirnioo  13480  ioorebas  13482  om2uzrani  13993  uzrdg0i  14000  hashunlei  14467  cats1fvn  14900  trclubi  15038  sgnrn  15140  4sqlem19  17027  dec2dvds  17127  mod2xnegi  17135  modsubi  17136  gcdi  17137  isstruct2  17213  smndex1gbas  18965  smndex1gid  18967  smndex1igid  18969  grppropstr  19024  nn0srg  21596  fermltlchr  21688  ltbval  22203  sn0topon  23164  indistop  23168  indisuni  23169  indistps2  23178  indistps2ALT  23180  restbas  23324  leordtval2  23378  iocpnfordt  23381  icomnfordt  23382  iooordt  23383  reordt  23384  dis1stc  23665  ptcmpfi  23979  ustfn  24368  ustn0  24387  retopbas  24926  blssioo  24961  xrtgioo  24973  zcld  24980  cnperf  24987  retopconn  24996  rembl  25708  mbfdm  25794  ismbf  25796  mbf0  25802  bddiblnc  26010  abelthlem9  26612  advlog  26828  advlogexp  26829  2irrexpq  26905  cxpcn3  26922  loglesqrt  26935  log2ub  27123  ppi1i  27341  cht2  27345  cht3  27346  bpos1lem  27455  lgslem4  27473  vmadivsum  27655  log2sumbnd  27717  selberg2  27724  selbergr  27741  nogt01o  27869  mulsproplem9  28326  1n0s  28550  n0fincut  28557  2nns  28620  istrkg2ld  28738  iscgrg  28790  ishpg  29050  ax5seglem7  29294  h2hva  31335  h2hsm  31336  h2hnm  31337  norm-ii-i  31498  hhshsslem2  31629  shincli  31723  chincli  31821  lnophdi  32363  imaelshi  32419  rnelshi  32420  bdophdi  32458  padct  33072  dfdec100  33183  dpadd2  33238  dpmul  33241  dpmul4  33242  nn0omnd  33673  nn0archi  33676  znfermltl  33690  ccfldextrr  34045  lmatfvlem  34214  rrhre  34420  sigaex  34509  br2base  34668  sxbrsigalem3  34671  carsgclctunlem3  34719  sitmcl  34750  rpsqrtcn  34989  hgt750lem  35047  hgt750lem2  35048  afsval  35070  kur14lem7  35712  retopsconn  35749  satfvsuclem1  35859  fmlasuc0  35884  hfuni  36684  neibastop2lem  36899  onint1  36988  ttcid  37031  bj-snfromadj  37708  topdifinffinlem  38021  poimirlem9  38308  poimirlem28  38327  poimirlem30  38329  poimirlem32  38331  ftc1cnnc  38371  cncfres  38444  scottexf  38845  lineset  40540  lautset  40884  pautsetN  40900  tendoset  41561  decpmulnc  43076  decpmul  43077  areaquad  43971  0fno  44189  finonex  44208  sblpnf  45048  lhe4.4ex1a  45067  fourierdlem62  46910  fourierdlem76  46924  lamberte  47653  65537prm  48356  11gbo  48568  bgoldbtbndlem1  48598  seppcld  49736  setc1onsubc  50408