Theorem eleq1i 2831

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 2828	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶)

Syntax hints:   ↔ wb 207   = wceq 1547   ∈ wcel 2119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-clel 2815

This theorem is referenced by:  eleq12i  2833  eqeltri  2836  eqneltri  2859  intexrab  5282  abssexg  5318  rmorabex  5406  otelxp  5669  xpsspw  5759  dfse2  6059  dfse3  6294  ordtri3or  6349  fressnfv  7110  fnotovb  7415  ovmpos  7511  abnex  7707  sucexb  7754  f1stres  7962  f2ndres  7963  elxp6  7972  ottpos  8183  dftpos4  8192  tfr2b  8332  tz7.48-3  8380  unfi  9102  difinf  9218  fiint  9234  infssuni  9253  fsuppunbi  9299  r1pwALT  9768  djuexb  9831  alephprc  10019  fin1a2lem12  10331  axcclem  10377  zorn2lem4  10419  zornn0g  10425  grothomex  10750  grothprimlem  10754  addclprlem2  10938  axicn  11071  0mnnnnn0  12467  fcdmnn0fsupp  12493  pfxccatin12lem3  14692  pfxccat3  14694  swrdccat  14695  pfxccat3a  14698  swrdccat3blem  14699  swrdccat3b  14700  harmonic  15822  nprmi  16656  issubmgm  18668  issubm  18769  idresefmnd  18865  mulgfval  19043  oppgsubm  19335  idrespermg  19384  issrg  20167  srgfcl  20175  subrngrng  20529  opprsubrng  20538  rhmimasubrng  20545  cntzsubrng  20546  opprsubrg  20572  rngridlmcl  21217  isridlrng  21219  isridl  21252  resubdrg  21590  cpmidpmat  22863  kgencn  23546  kgencn2  23547  txdis1cn  23625  qtopres  23688  qtopcn  23704  cfinfil  23883  tgphaus  24107  xmeterval  24422  blval2  24552  metuel2  24555  iscvsp  25120  zclmncvs  25140  caucfil  25275  resscdrg  25350  finiunmbl  25536  iblre  25786  dvfsumlem2  26019  logno1  26625  rlimcnp2  26955  ppi2i  27157  gausslemma2dlem1a  27353  2lgslem4  27394  noxp1o  27652  usgrexmpl  29357  usgredgffibi  29418  nbupgrel  29439  nbuhgr2vtx1edgb  29446  nbusgreledg  29447  nbusgrf1o0  29463  nb3grpr  29476  nb3grpr2  29477  nb3gr2nb  29478  cusgrsizeinds  29546  cusgrfi  29552  finsumvtxdg2size  29644  wlkp1lem1  29765  wlkp1lem7  29771  wlkp1lem8  29772  wwlks2onsym  30053  rusgrnumwwlks  30070  clwwlknclwwlkdifnum  30075  clwwlknonfin  30189  clwwlknonex2  30204  umgr3cyclex  30278  eupthp1  30311  eupth2eucrct  30312  frcond3  30364  frgr3v  30370  3vfriswmgr  30373  1to3vfriendship  30376  2pthfrgrrn  30377  3cyclfrgrrn1  30380  4cycl2v2nb  30384  frgrnbnb  30388  frgrncvvdeqlem3  30396  frgrncvvdeqlem6  30399  frgrhash2wsp  30427  fusgr2wsp2nb  30429  numclwwlk1  30456  avril1  30558  n0lplig  30579  hhph  31274  nonbooli  31747  pjss2i  31776  atssma  32474  isrrext  34191  hasheuni  34276  dmvlsiga  34320  measiuns  34408  eulerpartlemmf  34566  fissorduni  35278  fineqvrep  35302  onvf1odlem2  35339  onvf1odlem4  35341  cusgr3cyclex  35371  resconn  35481  cvmlift2lem9  35546  rdgprc0  36026  bj-snsetex  37323  bj-tagex  37347  bj-0int  37466  poimirlem30  38024  ftc1anclem3  38069  ftc1anclem6  38072  rrnheibor  38211  rngo1cl  38313  isdrngo1  38330  dfcoeleqvrels  39079  rnqmapeleldisjsim  39236  islpln2ah  40048  lhpocnel2  40518  cdlemg31b0N  41193  cdlemg31b0a  41194  cdlemh  41316  cdlemk19w  41471  aks4d1lem1  42554  sticksstones4  42641  mzpclval  43181  wopprc  43482  dfac21  43518  uniel  43669  sucomisnotcard  43995  binomcxplemdvsum  44806  binomcxp  44808  mccl  46050  fprodcn  46052  stoweidlem17  46467  fourierdlem89  46645  fourierdlem90  46646  fourierdlem91  46647  fourierdlem100  46656  omeiunltfirp  46969  hoidmvlelem5  47049  issmf  47178  issmff  47184  smflimlem4  47224  smflim  47227  smflim2  47256  smflimsuplem1  47270  smflimsuplem8  47277  smflimsup  47278  chnerlem1  47334  aiotaexb  47559  aiotavb  47560  aovvdm  47655  aovvfunressn  47657  aovrcl  47659  aovvoveq  47662  aov0nbovbi  47665  fnotaovb  47668  mod2addne  47840  prmdvdsfmtnof1lem1  48069  341fppr2  48232  9fppr8  48235  clnbupgrel  48332  grtriproplem  48437  grtrif1o  48440  grtriclwlk3  48443  usgrgrtrirex  48448  isubgr3stgrlem7  48470  grlimprclnbgr  48494  grlimprclnbgrvtx  48497  usgrexmpl1  48520  usgrexmpl2  48525  gpgvtxedg0  48561  gpgvtxedg1  48562  gpgedg2ov  48564  gpgedg2iv  48565  gpgprismgr4cycllem11  48603  pgnbgreunbgrlem1  48611  pgnbgreunbgrlem2lem3  48614  pgnbgreunbgrlem2  48615  pgnbgreunbgrlem4  48617  pgnbgreunbgrlem5  48621  pgnbgreunbgr  48623  pgn4cyclex  48624  zlmodzxzldeplem3  49000  itscnhlinecirc02p  49283  fonex  49364  idemb  49656