Theorem eleq1i 2828

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

Syntax hints:   ↔ wb 206   = wceq 1542   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812

This theorem is referenced by:  eleq12i  2830  eqeltri  2833  eqneltri  2856  intexrab  5284  abssexg  5319  rmorabex  5407  otelxp  5668  xpsspw  5758  dfse2  6059  dfse3  6294  ordtri3or  6349  fressnfv  7107  fnotovb  7412  ovmpos  7508  abnex  7704  sucexb  7751  f1stres  7959  f2ndres  7960  elxp6  7969  ottpos  8179  dftpos4  8188  tfr2b  8328  tz7.48-3  8376  unfi  9098  difinf  9214  fiint  9230  infssuni  9249  fsuppunbi  9295  r1pwALT  9761  djuexb  9824  alephprc  10012  fin1a2lem12  10324  axcclem  10370  zorn2lem4  10412  zornn0g  10418  grothomex  10743  grothprimlem  10747  addclprlem2  10931  axicn  11064  0mnnnnn0  12460  fcdmnn0fsupp  12486  pfxccatin12lem3  14685  pfxccat3  14687  swrdccat  14688  pfxccat3a  14691  swrdccat3blem  14692  swrdccat3b  14693  harmonic  15815  nprmi  16649  issubmgm  18661  issubm  18762  idresefmnd  18858  mulgfval  19036  oppgsubm  19328  idrespermg  19377  issrg  20160  srgfcl  20168  subrngrng  20518  opprsubrng  20527  rhmimasubrng  20534  cntzsubrng  20535  opprsubrg  20561  rngridlmcl  21207  isridlrng  21209  isridl  21242  resubdrg  21598  cpmidpmat  22848  kgencn  23531  kgencn2  23532  txdis1cn  23610  qtopres  23673  qtopcn  23689  cfinfil  23868  tgphaus  24092  xmeterval  24407  blval2  24537  metuel2  24540  iscvsp  25105  zclmncvs  25125  caucfil  25260  resscdrg  25335  finiunmbl  25521  iblre  25771  dvfsumlem2  26004  logno1  26613  rlimcnp2  26943  ppi2i  27146  gausslemma2dlem1a  27342  2lgslem4  27383  noxp1o  27641  usgrexmpl  29346  usgredgffibi  29407  nbupgrel  29428  nbuhgr2vtx1edgb  29435  nbusgreledg  29436  nbusgrf1o0  29452  nb3grpr  29465  nb3grpr2  29466  nb3gr2nb  29467  cusgrsizeinds  29536  cusgrfi  29542  finsumvtxdg2size  29634  wlkp1lem1  29755  wlkp1lem7  29761  wlkp1lem8  29762  wwlks2onsym  30043  rusgrnumwwlks  30060  clwwlknclwwlkdifnum  30065  clwwlknonfin  30179  clwwlknonex2  30194  umgr3cyclex  30268  eupthp1  30301  eupth2eucrct  30302  frcond3  30354  frgr3v  30360  3vfriswmgr  30363  1to3vfriendship  30366  2pthfrgrrn  30367  3cyclfrgrrn1  30370  4cycl2v2nb  30374  frgrnbnb  30378  frgrncvvdeqlem3  30386  frgrncvvdeqlem6  30389  frgrhash2wsp  30417  fusgr2wsp2nb  30419  numclwwlk1  30446  avril1  30548  n0lplig  30569  hhph  31264  nonbooli  31737  pjss2i  31766  atssma  32464  isrrext  34160  hasheuni  34245  dmvlsiga  34289  measiuns  34377  eulerpartlemmf  34535  fissorduni  35249  fineqvrep  35274  onvf1odlem2  35302  onvf1odlem4  35304  cusgr3cyclex  35334  resconn  35444  cvmlift2lem9  35509  rdgprc0  35989  bj-snsetex  37286  bj-tagex  37310  bj-0int  37429  poimirlem30  37985  ftc1anclem3  38030  ftc1anclem6  38033  rrnheibor  38172  rngo1cl  38274  isdrngo1  38291  dfcoeleqvrels  39040  rnqmapeleldisjsim  39197  islpln2ah  40009  lhpocnel2  40479  cdlemg31b0N  41154  cdlemg31b0a  41155  cdlemh  41277  cdlemk19w  41432  aks4d1lem1  42515  sticksstones4  42602  mzpclval  43171  wopprc  43476  dfac21  43512  uniel  43663  sucomisnotcard  43989  binomcxplemdvsum  44800  binomcxp  44802  mccl  46046  fprodcn  46048  stoweidlem17  46463  fourierdlem89  46641  fourierdlem90  46642  fourierdlem91  46643  fourierdlem100  46652  omeiunltfirp  46965  hoidmvlelem5  47045  issmf  47174  issmff  47180  smflimlem4  47220  smflim  47223  smflim2  47252  smflimsuplem1  47266  smflimsuplem8  47273  smflimsup  47274  chnerlem1  47328  aiotaexb  47549  aiotavb  47550  aovvdm  47645  aovvfunressn  47647  aovrcl  47649  aovvoveq  47652  aov0nbovbi  47655  fnotaovb  47658  mod2addne  47830  prmdvdsfmtnof1lem1  48059  341fppr2  48222  9fppr8  48225  clnbupgrel  48322  grtriproplem  48427  grtrif1o  48430  grtriclwlk3  48433  usgrgrtrirex  48438  isubgr3stgrlem7  48460  grlimprclnbgr  48484  grlimprclnbgrvtx  48487  usgrexmpl1  48510  usgrexmpl2  48515  gpgvtxedg0  48551  gpgvtxedg1  48552  gpgedg2ov  48554  gpgedg2iv  48555  gpgprismgr4cycllem11  48593  pgnbgreunbgrlem1  48601  pgnbgreunbgrlem2lem3  48604  pgnbgreunbgrlem2  48605  pgnbgreunbgrlem4  48607  pgnbgreunbgrlem5  48611  pgnbgreunbgr  48613  pgn4cyclex  48614  zlmodzxzldeplem3  48990  itscnhlinecirc02p  49273  fonex  49354  idemb  49646