Theorem eleq1i 2860

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

Syntax hints:   ↔ wb 209   = wceq 1567   ∈ wcel 2149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-clel 2844

This theorem is referenced by:  eleq12i  2862  eqeltri  2865  eqneltri  2888  intexrab  5315  abssexg  5351  rmorabex  5439  otelxp  5703  xpsspw  5794  dfse2  6100  dfse3  6334  ordtri3or  6390  fressnfv  7155  fnotovb  7460  ovmpos  7556  abnex  7752  sucexb  7799  f1stres  8006  f2ndres  8007  elxp6  8016  ottpos  8228  dftpos4  8237  tfr2b  8379  tz7.48-3  8427  unfi  9151  difinf  9267  fiint  9282  infssuni  9299  fsuppunbi  9345  r1pwALT  9814  djuexb  9891  alephprc  10079  fin1a2lem12  10391  axcclem  10437  zorn2lem4  10479  zornn0g  10485  grothomex  10810  grothprimlem  10814  addclprlem2  10998  axicn  11131  0mnnnnn0  12532  fcdmnn0fsupp  12558  pfxccatin12lem3  14765  pfxccat3  14767  swrdccat  14768  pfxccat3a  14771  swrdccat3blem  14772  swrdccat3b  14773  harmonic  15909  nprmi  16743  issubmgm  18756  issubm  18857  idresefmnd  18954  mulgfval  19131  oppgsubm  19428  idrespermg  19477  issrg  20266  srgfcl  20274  subrngrng  20631  opprsubrng  20640  rhmimasubrng  20647  cntzsubrng  20648  opprsubrg  20674  rngridlmcl  21316  isridlrng  21318  isridl  21358  resubdrg  21723  cpmidpmat  22995  kgencn  23678  kgencn2  23679  txdis1cn  23757  qtopres  23820  qtopcn  23836  cfinfil  24015  tgphaus  24239  xmeterval  24554  blval2  24684  metuel2  24687  iscvsp  25252  zclmncvs  25272  caucfil  25407  resscdrg  25482  finiunmbl  25668  iblre  25918  dvfsumlem2  26151  logno1  26763  rlimcnp2  27093  ppi2i  27295  gausslemma2dlem1a  27491  2lgslem4  27532  noxp1o  27789  usgrexmpl  29550  usgredgffibi  29611  nbupgrel  29632  nbuhgr2vtx1edgb  29639  nbusgreledg  29640  nbusgrf1o0  29656  nb3grpr  29669  nb3grpr2  29670  nb3gr2nb  29671  cusgrsizeinds  29739  cusgrfi  29745  finsumvtxdg2size  29837  wlkp1lem1  29958  wlkp1lem7  29964  wlkp1lem8  29965  wwlks2onsym  30246  rusgrnumwwlks  30263  clwwlknclwwlkdifnum  30268  clwwlknonfin  30382  clwwlknonex2  30397  umgr3cyclex  30471  eupthp1  30504  eupth2eucrct  30505  frcond3  30557  frgr3v  30563  3vfriswmgr  30566  1to3vfriendship  30569  2pthfrgrrn  30570  3cyclfrgrrn1  30573  4cycl2v2nb  30577  frgrnbnb  30581  frgrncvvdeqlem3  30589  frgrncvvdeqlem6  30592  frgrhash2wsp  30620  fusgr2wsp2nb  30622  numclwwlk1  30649  avril1  30751  n0lplig  30772  hhph  31467  nonbooli  31940  pjss2i  31969  atssma  32667  isrrext  34331  hasheuni  34416  dmvlsiga  34460  measiuns  34548  eulerpartlemmf  34706  fissorduni  35419  fineqvrep  35446  onvf1odlem2  35483  onvf1odlem4  35485  cusgr3cyclex  35523  resconn  35633  cvmlift2lem9  35698  rdgprc0  36178  bj-snsetex  37483  bj-tagex  37507  bj-0int  37626  poimirlem30  38184  ftc1anclem3  38229  ftc1anclem6  38232  rrnheibor  38371  rngo1cl  38473  isdrngo1  38490  dfcoeleqvrels  39239  rnqmapeleldisjsim  39396  islpln2ah  40208  lhpocnel2  40678  cdlemg31b0N  41353  cdlemg31b0a  41354  cdlemh  41476  cdlemk19w  41631  aks4d1lem1  42714  sticksstones4  42801  mzpclval  43341  wopprc  43642  dfac21  43678  uniel  43829  sucomisnotcard  44155  binomcxplemdvsum  44950  binomcxp  44952  mccl  46199  fprodcn  46201  stoweidlem17  46616  fourierdlem89  46794  fourierdlem90  46795  fourierdlem91  46796  fourierdlem100  46805  omeiunltfirp  47118  hoidmvlelem5  47198  issmf  47327  issmff  47333  smflimlem4  47373  smflim  47376  smflim2  47405  smflimsuplem1  47419  smflimsuplem8  47426  smflimsup  47427  chnerlem1  47483  aiotaexb  47708  aiotavb  47709  aovvdm  47804  aovvfunressn  47806  aovrcl  47808  aovvoveq  47811  aov0nbovbi  47814  fnotaovb  47817  mod2addne  47989  prmdvdsfmtnof1lem1  48218  341fppr2  48381  9fppr8  48384  clnbupgrel  48481  grtriproplem  48586  grtrif1o  48589  grtriclwlk3  48592  usgrgrtrirex  48597  isubgr3stgrlem7  48619  grlimprclnbgr  48643  grlimprclnbgrvtx  48646  usgrexmpl1  48669  usgrexmpl2  48674  gpgvtxedg0  48710  gpgvtxedg1  48711  gpgedg2ov  48713  gpgedg2iv  48714  gpgprismgr4cycllem11  48752  pgnbgreunbgrlem1  48760  pgnbgreunbgrlem2lem3  48763  pgnbgreunbgrlem2  48764  pgnbgreunbgrlem4  48766  pgnbgreunbgrlem5  48770  pgnbgreunbgr  48772  pgn4cyclex  48773  zlmodzxzldeplem3  49160  itscnhlinecirc02p  49443  fonex  49523  idemb  49815