Theorem eleq1i 2856

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ∈ wcel 2146

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-clel 2840

This theorem is used by:  eleq12i  2858  eqeltri  2861  eqneltri  2884  intexrab  5319  abssexg  5355  rmorabex  5443  otelxp  5707  xpsspw  5798  dfse2  6104  dfse3  6341  ordtri3or  6397  fressnfv  7161  fnotovb  7468  ovmpos  7564  abnex  7758  sucexb  7805  f1stres  8012  f2ndres  8013  elxp6  8022  ottpos  8234  dftpos4  8243  tfr2b  8385  tz7.48-3  8433  unfi  9158  difinf  9274  fiint  9289  infssuni  9306  fsuppunbi  9352  r1pwALT  9821  djuexb  9907  alephprc  10095  fin1a2lem12  10406  axcclem  10452  zorn2lem4  10494  zornn0g  10500  grothomex  10825  grothprimlem  10829  addclprlem2  11013  axicn  11146  0mnnnnn0  12547  fcdmnn0fsupp  12573  pfxccatin12lem3  14786  pfxccat3  14788  swrdccat  14789  pfxccat3a  14792  swrdccat3blem  14793  swrdccat3b  14794  harmonic  15931  nprmi  16764  issubmgm  18781  issubm  18884  idresefmnd  18981  mulgfval  19158  oppgsubm  19455  idrespermg  19504  issrg  20293  srgfcl  20301  subrngrng  20678  opprsubrng  20687  rhmimasubrng  20694  cntzsubrng  20695  opprsubrg  20721  rngridlmcl  21371  isridlrng  21373  isridl  21420  resubdrg  21787  cpmidpmat  23059  kgencn  23742  kgencn2  23743  txdis1cn  23821  qtopres  23884  qtopcn  23900  cfinfil  24079  tgphaus  24303  xmeterval  24618  blval2  24748  metuel2  24751  iscvsp  25316  zclmncvs  25336  caucfil  25471  resscdrg  25546  finiunmbl  25732  iblre  25982  dvfsumlem2  26215  logno1  26830  rlimcnp2  27160  ppi2i  27362  gausslemma2dlem1a  27558  2lgslem4  27599  noxp1o  27856  usgrexmpl  29642  usgredgffibi  29703  nbupgrel  29724  nbuhgr2vtx1edgb  29731  nbusgreledg  29732  nbusgrf1o0  29748  nb3grpr  29761  nb3grpr2  29762  nb3gr2nb  29763  cusgrsizeinds  29831  cusgrfi  29837  finsumvtxdg2size  29929  wlkp1lem1  30050  wlkp1lem7  30056  wlkp1lem8  30057  wwlks2onsym  30338  rusgrnumwwlks  30355  clwwlknclwwlkdifnum  30360  clwwlknonfin  30474  clwwlknonex2  30489  umgr3cyclex  30563  eupthp1  30596  eupth2eucrct  30597  frcond3  30649  frgr3v  30655  3vfriswmgr  30658  1to3vfriendship  30661  2pthfrgrrn  30662  3cyclfrgrrn1  30665  4cycl2v2nb  30669  frgrnbnb  30673  frgrncvvdeqlem3  30681  frgrncvvdeqlem6  30684  frgrhash2wsp  30712  fusgr2wsp2nb  30714  numclwwlk1  30741  avril1  30843  n0lplig  30864  hhph  31559  nonbooli  32032  pjss2i  32061  atssma  32759  isrrext  34413  hasheuni  34498  dmvlsiga  34542  measiuns  34631  eulerpartlemmf  34789  fissorduni  35497  fineqvrep  35543  onvf1odlem2  35604  onvf1odlem4  35606  cusgr3cyclex  35641  resconn  35751  cvmlift2lem9  35816  rdgprc0  36296  bj-snsetex  37632  bj-tagex  37656  bj-0int  37776  poimirlem30  38334  ftc1anclem3  38379  ftc1anclem6  38382  rrnheibor  38521  rngo1cl  38623  isdrngo1  38640  dfcoeleqvrels  39387  rnqmapeleldisjsim  39544  islpln2ah  40356  lhpocnel2  40826  cdlemg31b0N  41501  cdlemg31b0a  41502  cdlemh  41624  cdlemk19w  41779  aks4d1lem1  42862  sticksstones4  42949  mzpclval  43489  wopprc  43790  dfac21  43826  uniel  43977  sucomisnotcard  44303  binomcxplemdvsum  45098  binomcxp  45100  mccl  46347  fprodcn  46349  stoweidlem17  46764  fourierdlem89  46942  fourierdlem90  46943  fourierdlem91  46944  fourierdlem100  46953  omeiunltfirp  47266  hoidmvlelem5  47346  issmf  47475  issmff  47481  smflimlem4  47521  smflim  47524  smflim2  47553  smflimsuplem1  47567  smflimsuplem8  47574  smflimsup  47575  chnerlem1  47631  aiotaexb  47859  aiotavb  47860  aovvdm  47955  aovvfunressn  47957  aovrcl  47959  aovvoveq  47962  aov0nbovbi  47965  fnotaovb  47968  mod2addne  48140  prmdvdsfmtnof1lem1  48369  341fppr2  48532  9fppr8  48535  clnbupgrel  48632  grtriproplem  48737  grtrif1o  48740  grtriclwlk3  48743  usgrgrtrirex  48748  isubgr3stgrlem7  48770  grlimprclnbgr  48794  grlimprclnbgrvtx  48797  usgrexmpl1  48820  usgrexmpl2  48825  gpgvtxedg0  48861  gpgvtxedg1  48862  gpgedg2ov  48864  gpgedg2iv  48865  gpgprismgr4cycllem11  48903  pgnbgreunbgrlem1  48911  pgnbgreunbgrlem2lem3  48914  pgnbgreunbgrlem2  48915  pgnbgreunbgrlem4  48917  pgnbgreunbgrlem5  48921  pgnbgreunbgr  48923  pgn4cyclex  48924  zlmodzxzldeplem3  49315  itscnhlinecirc02p  49598  fonex  49678  idemb  49970