Theorem eleq1i 2825

Description: Inference from equality to equivalence of membership. (Contributed by NM, 21-Jun-1993.)

Hypothesis

Ref	Expression
eleq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
eleq1i	⊢ (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶)

Proof of Theorem eleq1i

Step	Hyp	Ref	Expression
1		eleq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		eleq1 2822	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶)

Syntax hints:   ↔ wb 205   = wceq 1542   ∈ wcel 2107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-clel 2811

This theorem is referenced by:  eleq12i  2827  eqeltri  2830  eqneltri  2853  intexrab  5341  abssexg  5381  rmorabex  5461  otelxp  5721  xpsspw  5810  dfse2  6100  dfse3  6338  ordtri3or  6397  fressnfv  7158  fnotovb  7459  ovmpos  7556  abnex  7744  sucexb  7792  f1stres  7999  f2ndres  8000  elxp6  8009  ottpos  8221  dftpos4  8230  tfr2b  8396  tz7.48-3  8444  unfi  9172  difinf  9316  fiint  9324  infssuni  9343  fsuppunbi  9384  r1pwALT  9841  djuexb  9904  alephprc  10094  fin1a2lem12  10406  axcclem  10452  zorn2lem4  10494  zornn0g  10500  grothomex  10824  grothprimlem  10828  addclprlem2  11012  axicn  11145  0mnnnnn0  12504  fcdmnn0fsupp  12529  pfxccatin12lem3  14682  pfxccat3  14684  swrdccat  14685  pfxccat3a  14688  swrdccat3blem  14689  swrdccat3b  14690  harmonic  15805  nprmi  16626  issubm  18684  idresefmnd  18780  mulgfval  18952  oppgsubm  19229  idrespermg  19279  issrg  20011  srgfcl  20019  opprsubrg  20340  isridl  20859  resubdrg  21161  cpmidpmat  22375  kgencn  23060  kgencn2  23061  txdis1cn  23139  qtopres  23202  qtopcn  23218  cfinfil  23397  tgphaus  23621  xmeterval  23938  blval2  24071  metuel2  24074  iscvsp  24644  zclmncvs  24665  caucfil  24800  resscdrg  24875  finiunmbl  25061  iblre  25311  logno1  26144  rlimcnp2  26471  ppi2i  26673  gausslemma2dlem1a  26868  2lgslem4  26909  noxp1o  27166  usgredgffibi  28581  nbupgrel  28602  nbuhgr2vtx1edgb  28609  nbusgreledg  28610  nbusgrf1o0  28626  nb3grpr  28639  nb3grpr2  28640  nb3gr2nb  28641  cusgrsizeinds  28709  cusgrfi  28715  finsumvtxdg2size  28807  wlkp1lem1  28930  wlkp1lem7  28936  wlkp1lem8  28937  wwlks2onsym  29212  rusgrnumwwlks  29228  clwwlknclwwlkdifnum  29233  clwwlknonfin  29347  clwwlknonex2  29362  umgr3cyclex  29436  eupthp1  29469  eupth2eucrct  29470  frcond3  29522  frgr3v  29528  3vfriswmgr  29531  1to3vfriendship  29534  2pthfrgrrn  29535  3cyclfrgrrn1  29538  4cycl2v2nb  29542  frgrnbnb  29546  frgrncvvdeqlem3  29554  frgrncvvdeqlem6  29557  frgrhash2wsp  29585  fusgr2wsp2nb  29587  numclwwlk1  29614  avril1  29716  n0lplig  29736  hhph  30431  nonbooli  30904  pjss2i  30933  atssma  31631  isrrext  32980  hasheuni  33083  dmvlsiga  33127  measiuns  33215  eulerpartlemmf  33374  fineqvrep  34095  cusgr3cyclex  34127  resconn  34237  cvmlift2lem9  34302  rdgprc0  34765  gg-dvfsumlem2  35183  bj-snsetex  35844  bj-tagex  35868  bj-0int  35982  poimirlem30  36518  ftc1anclem3  36563  ftc1anclem6  36566  rrnheibor  36705  rngo1cl  36807  isdrngo1  36824  dfcoeleqvrels  37491  islpln2ah  38420  lhpocnel2  38890  cdlemg31b0N  39565  cdlemg31b0a  39566  cdlemh  39688  cdlemk19w  39843  aks4d1lem1  40927  sticksstones4  40965  mzpclval  41463  wopprc  41769  dfac21  41808  uniel  41966  sucomisnotcard  42295  binomcxplemdvsum  43114  binomcxp  43116  mccl  44314  fprodcn  44316  stoweidlem17  44733  fourierdlem89  44911  fourierdlem90  44912  fourierdlem91  44913  fourierdlem100  44922  omeiunltfirp  45235  hoidmvlelem5  45315  issmf  45444  issmff  45450  smflimlem4  45490  smflim  45493  smflim2  45522  smflimsuplem1  45536  smflimsuplem8  45543  smflimsup  45544  aiotaexb  45797  aiotavb  45798  aovvdm  45893  aovvfunressn  45895  aovrcl  45897  aovvoveq  45900  aov0nbovbi  45903  fnotaovb  45906  prmdvdsfmtnof1lem1  46252  341fppr2  46402  9fppr8  46405  issubmgm  46559  subrngrng  46729  opprsubrng  46738  rhmimasubrng  46745  cntzsubrng  46746  rngridlmcl  46749  isridlrng  46751  zlmodzxzldeplem3  47183  itscnhlinecirc02p  47471