Theorem eleq1i 2851

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

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

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 2147  ax-9 2155  ax-ext 2732

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

This theorem is used by:  eleq12i  2853  eqeltri  2856  eqneltri  2879  intexrab  5311  abssexg  5347  rmorabex  5435  otelxp  5699  xpsspw  5790  dfse2  6096  dfse3  6334  ordtri3or  6390  fressnfv  7157  fnotovb  7465  ovmpos  7561  abnex  7756  sucexb  7803  f1stres  8010  f2ndres  8011  elxp6  8020  ottpos  8234  dftpos4  8243  tfr2b  8385  tz7.48-3  8433  unfi  9165  difinf  9281  fiint  9296  infssuni  9313  fsuppunbi  9359  r1pwALT  9828  djuexb  9914  alephprc  10102  fin1a2lem12  10413  axcclem  10459  zorn2lem4  10501  zornn0g  10507  grothomex  10838  grothprimlem  10842  addclprlem2  11026  axicn  11159  0mnnnnn0  12560  fcdmnn0fsupp  12586  pfxccatin12lem3  14801  pfxccat3  14803  swrdccat  14804  pfxccat3a  14807  swrdccat3blem  14808  swrdccat3b  14809  harmonic  15948  nprmi  16779  issubmgm  18804  issubm  18911  idresefmnd  19008  mulgfval  19192  oppgsubm  19489  idrespermg  19538  issrg  20327  srgfcl  20335  subrngrng  20712  opprsubrng  20721  rhmimasubrng  20728  cntzsubrng  20729  opprsubrg  20755  rngridlmcl  21405  isridlrng  21407  isridl  21454  resubdrg  21821  cpmidpmat  23098  kgencn  23782  kgencn2  23783  txdis1cn  23861  qtopres  23924  qtopcn  23940  cfinfil  24119  tgphaus  24343  xmeterval  24658  blval2  24788  metuel2  24791  iscvsp  25356  zclmncvs  25376  caucfil  25511  resscdrg  25586  finiunmbl  25772  iblre  26021  dvfsumlem2  26254  logno1  26873  rlimcnp2  27203  ppi2i  27405  gausslemma2dlem1a  27601  2lgslem4  27642  noxp1o  27899  usgrexmpl  29723  usgredgffibi  29784  nbupgrel  29805  nbuhgr2vtx1edgb  29812  nbusgreledg  29813  nbusgrf1o0  29829  nb3grpr  29842  nb3grpr2  29843  nb3gr2nb  29844  cusgrsizeinds  29912  cusgrfi  29918  finsumvtxdg2size  30010  wlkp1lem1  30131  wlkp1lem7  30137  wlkp1lem8  30138  wwlks2onsym  30428  rusgrnumwwlks  30445  clwwlknclwwlkdifnum  30450  clwwlknonfin  30564  clwwlknonex2  30579  umgr3cyclex  30663  eupthp1  30696  eupth2eucrct  30697  frcond3  30749  frgr3v  30755  3vfriswmgr  30758  1to3vfriendship  30761  2pthfrgrrn  30762  3cyclfrgrrn1  30765  4cycl2v2nb  30769  frgrnbnb  30773  frgrncvvdeqlem3  30781  frgrncvvdeqlem6  30784  frgrhash2wsp  30812  fusgr2wsp2nb  30814  numclwwlk1  30841  avril1  30943  n0lplig  30964  hhph  31659  nonbooli  32132  pjss2i  32161  atssma  32859  isrrext  34510  hasheuni  34595  dmvlsiga  34639  measiuns  34728  eulerpartlemmf  34886  fissorduni  35594  fineqvrep  35640  onvf1odlem2  35701  onvf1odlem4  35703  cusgr3cyclex  35725  resconn  35825  cvmlift2lem9  35890  rdgprc0  36370  bj-snsetex  37707  bj-tagex  37731  bj-0int  37851  poimirlem30  38399  ftc1anclem3  38444  ftc1anclem6  38447  rrnheibor  38587  rngo1cl  38689  isdrngo1  38706  dfcoeleqvrels  39453  rnqmapeleldisjsim  39610  islpln2ah  40422  lhpocnel2  40892  cdlemg31b0N  41567  cdlemg31b0a  41568  cdlemh  41690  cdlemk19w  41845  aks4d1lem1  42928  sticksstones4  43015  mzpclval  43570  wopprc  43871  dfac21  43907  uniel  44058  sucomisnotcard  44384  binomcxplemdvsum  45179  binomcxp  45181  mccl  46428  fprodcn  46430  stoweidlem17  46845  fourierdlem89  47023  fourierdlem90  47024  fourierdlem91  47025  fourierdlem100  47034  omeiunltfirp  47347  hoidmvlelem5  47427  issmf  47556  issmff  47562  smflimlem4  47602  smflim  47605  smflim2  47634  smflimsuplem1  47648  smflimsuplem8  47655  smflimsup  47656  aiotaexb  47977  aiotavb  47978  aovvdm  48073  aovvfunressn  48075  aovrcl  48077  aovvoveq  48080  aov0nbovbi  48083  fnotaovb  48086  mod2addne  48258  prmdvdsfmtnof1lem1  48487  341fppr2  48650  9fppr8  48653  clnbupgrel  48750  grtriproplem  48855  grtrif1o  48858  grtriclwlk3  48861  usgrgrtrirex  48866  isubgr3stgrlem7  48888  grlimprclnbgr  48912  grlimprclnbgrvtx  48915  usgrexmpl1  48938  usgrexmpl2  48943  gpgvtxedg0  48979  gpgvtxedg1  48980  gpgedg2ov  48982  gpgedg2iv  48983  gpgprismgr4cycllem11  49021  pgnbgreunbgrlem1  49029  pgnbgreunbgrlem2lem3  49032  pgnbgreunbgrlem2  49033  pgnbgreunbgrlem4  49035  pgnbgreunbgrlem5  49039  pgnbgreunbgr  49041  pgn4cyclex  49042  zlmodzxzldeplem3  49432  itscnhlinecirc02p  49715  fonex  49795  idemb  50085  dvsec  50689  dvcsc  50690  dvcot  50691