Theorem eleq1i 2819

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

Syntax hints:   ↔ wb 206   = wceq 1540   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803

This theorem is referenced by:  eleq12i  2821  eqeltri  2824  eqneltri  2847  intexrab  5297  abssexg  5332  rmorabex  5415  otelxp  5675  xpsspw  5763  dfse2  6060  dfse3  6297  ordtri3or  6352  fressnfv  7114  fnotovb  7421  ovmpos  7517  abnex  7713  sucexb  7760  f1stres  7971  f2ndres  7972  elxp6  7981  ottpos  8192  dftpos4  8201  tfr2b  8341  tz7.48-3  8389  unfi  9112  difinf  9236  fiint  9253  fiintOLD  9254  infssuni  9273  fsuppunbi  9316  r1pwALT  9775  djuexb  9838  alephprc  10028  fin1a2lem12  10340  axcclem  10386  zorn2lem4  10428  zornn0g  10434  grothomex  10758  grothprimlem  10762  addclprlem2  10946  axicn  11079  0mnnnnn0  12450  fcdmnn0fsupp  12476  pfxccatin12lem3  14673  pfxccat3  14675  swrdccat  14676  pfxccat3a  14679  swrdccat3blem  14680  swrdccat3b  14681  harmonic  15801  nprmi  16635  issubmgm  18605  issubm  18706  idresefmnd  18802  mulgfval  18977  oppgsubm  19270  idrespermg  19317  issrg  20073  srgfcl  20081  subrngrng  20435  opprsubrng  20444  rhmimasubrng  20451  cntzsubrng  20452  opprsubrg  20478  rngridlmcl  21103  isridlrng  21105  isridl  21138  resubdrg  21493  cpmidpmat  22736  kgencn  23419  kgencn2  23420  txdis1cn  23498  qtopres  23561  qtopcn  23577  cfinfil  23756  tgphaus  23980  xmeterval  24296  blval2  24426  metuel2  24429  iscvsp  25004  zclmncvs  25024  caucfil  25159  resscdrg  25234  finiunmbl  25421  iblre  25671  dvfsumlem2  25909  logno1  26521  rlimcnp2  26852  ppi2i  27055  gausslemma2dlem1a  27252  2lgslem4  27293  noxp1o  27551  usgrexmpl  29166  usgredgffibi  29227  nbupgrel  29248  nbuhgr2vtx1edgb  29255  nbusgreledg  29256  nbusgrf1o0  29272  nb3grpr  29285  nb3grpr2  29286  nb3gr2nb  29287  cusgrsizeinds  29356  cusgrfi  29362  finsumvtxdg2size  29454  wlkp1lem1  29575  wlkp1lem7  29581  wlkp1lem8  29582  wwlks2onsym  29861  rusgrnumwwlks  29877  clwwlknclwwlkdifnum  29882  clwwlknonfin  29996  clwwlknonex2  30011  umgr3cyclex  30085  eupthp1  30118  eupth2eucrct  30119  frcond3  30171  frgr3v  30177  3vfriswmgr  30180  1to3vfriendship  30183  2pthfrgrrn  30184  3cyclfrgrrn1  30187  4cycl2v2nb  30191  frgrnbnb  30195  frgrncvvdeqlem3  30203  frgrncvvdeqlem6  30206  frgrhash2wsp  30234  fusgr2wsp2nb  30236  numclwwlk1  30263  avril1  30365  n0lplig  30385  hhph  31080  nonbooli  31553  pjss2i  31582  atssma  32280  isrrext  33963  hasheuni  34048  dmvlsiga  34092  measiuns  34180  eulerpartlemmf  34339  fineqvrep  35058  onvf1odlem2  35064  onvf1odlem4  35066  cusgr3cyclex  35096  resconn  35206  cvmlift2lem9  35271  rdgprc0  35754  bj-snsetex  36924  bj-tagex  36948  bj-0int  37062  poimirlem30  37617  ftc1anclem3  37662  ftc1anclem6  37665  rrnheibor  37804  rngo1cl  37906  isdrngo1  37923  dfcoeleqvrels  38585  islpln2ah  39516  lhpocnel2  39986  cdlemg31b0N  40661  cdlemg31b0a  40662  cdlemh  40784  cdlemk19w  40939  aks4d1lem1  42023  sticksstones4  42110  mzpclval  42686  wopprc  42992  dfac21  43028  uniel  43179  sucomisnotcard  43506  binomcxplemdvsum  44317  binomcxp  44319  mccl  45569  fprodcn  45571  stoweidlem17  45988  fourierdlem89  46166  fourierdlem90  46167  fourierdlem91  46168  fourierdlem100  46177  omeiunltfirp  46490  hoidmvlelem5  46570  issmf  46699  issmff  46705  smflimlem4  46745  smflim  46748  smflim2  46777  smflimsuplem1  46791  smflimsuplem8  46798  smflimsup  46799  aiotaexb  47063  aiotavb  47064  aovvdm  47159  aovvfunressn  47161  aovrcl  47163  aovvoveq  47166  aov0nbovbi  47169  fnotaovb  47172  mod2addne  47338  prmdvdsfmtnof1lem1  47558  341fppr2  47708  9fppr8  47711  clnbupgrel  47808  grtriproplem  47911  grtrif1o  47914  grtriclwlk3  47917  usgrgrtrirex  47922  isubgr3stgrlem7  47944  usgrexmpl1  47986  usgrexmpl2  47991  gpgvtxedg0  48027  gpgvtxedg1  48028  gpgedg2ov  48030  gpgedg2iv  48031  gpgprismgr4cycllem11  48068  pgnbgreunbgrlem1  48076  pgnbgreunbgrlem2lem3  48079  pgnbgreunbgrlem2  48080  pgnbgreunbgrlem4  48082  pgnbgreunbgrlem5  48086  pgnbgreunbgr  48088  pgn4cyclex  48089  zlmodzxzldeplem3  48464  itscnhlinecirc02p  48747  fonex  48828  idemb  49121