Theorem eleq1i 2824

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

Syntax hints:   ↔ wb 206   = wceq 1541   ∈ wcel 2113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-clel 2808

This theorem is referenced by:  eleq12i  2826  eqeltri  2829  eqneltri  2852  intexrab  5289  abssexg  5324  rmorabex  5405  otelxp  5665  xpsspw  5755  dfse2  6056  dfse3  6291  ordtri3or  6346  fressnfv  7102  fnotovb  7407  ovmpos  7503  abnex  7699  sucexb  7746  f1stres  7954  f2ndres  7955  elxp6  7964  ottpos  8175  dftpos4  8184  tfr2b  8324  tz7.48-3  8372  unfi  9091  difinf  9206  fiint  9222  infssuni  9241  fsuppunbi  9284  r1pwALT  9750  djuexb  9813  alephprc  10001  fin1a2lem12  10313  axcclem  10359  zorn2lem4  10401  zornn0g  10407  grothomex  10731  grothprimlem  10735  addclprlem2  10919  axicn  11052  0mnnnnn0  12424  fcdmnn0fsupp  12450  pfxccatin12lem3  14646  pfxccat3  14648  swrdccat  14649  pfxccat3a  14652  swrdccat3blem  14653  swrdccat3b  14654  harmonic  15773  nprmi  16607  issubmgm  18618  issubm  18719  idresefmnd  18815  mulgfval  18990  oppgsubm  19282  idrespermg  19331  issrg  20114  srgfcl  20122  subrngrng  20474  opprsubrng  20483  rhmimasubrng  20490  cntzsubrng  20491  opprsubrg  20517  rngridlmcl  21163  isridlrng  21165  isridl  21198  resubdrg  21554  cpmidpmat  22808  kgencn  23491  kgencn2  23492  txdis1cn  23570  qtopres  23633  qtopcn  23649  cfinfil  23828  tgphaus  24052  xmeterval  24367  blval2  24497  metuel2  24500  iscvsp  25075  zclmncvs  25095  caucfil  25230  resscdrg  25305  finiunmbl  25492  iblre  25742  dvfsumlem2  25980  logno1  26592  rlimcnp2  26923  ppi2i  27126  gausslemma2dlem1a  27323  2lgslem4  27364  noxp1o  27622  usgrexmpl  29262  usgredgffibi  29323  nbupgrel  29344  nbuhgr2vtx1edgb  29351  nbusgreledg  29352  nbusgrf1o0  29368  nb3grpr  29381  nb3grpr2  29382  nb3gr2nb  29383  cusgrsizeinds  29452  cusgrfi  29458  finsumvtxdg2size  29550  wlkp1lem1  29671  wlkp1lem7  29677  wlkp1lem8  29678  wwlks2onsym  29959  rusgrnumwwlks  29976  clwwlknclwwlkdifnum  29981  clwwlknonfin  30095  clwwlknonex2  30110  umgr3cyclex  30184  eupthp1  30217  eupth2eucrct  30218  frcond3  30270  frgr3v  30276  3vfriswmgr  30279  1to3vfriendship  30282  2pthfrgrrn  30283  3cyclfrgrrn1  30286  4cycl2v2nb  30290  frgrnbnb  30294  frgrncvvdeqlem3  30302  frgrncvvdeqlem6  30305  frgrhash2wsp  30333  fusgr2wsp2nb  30335  numclwwlk1  30362  avril1  30464  n0lplig  30484  hhph  31179  nonbooli  31652  pjss2i  31681  atssma  32379  isrrext  34085  hasheuni  34170  dmvlsiga  34214  measiuns  34302  eulerpartlemmf  34460  fissorduni  35173  fineqvrep  35209  onvf1odlem2  35220  onvf1odlem4  35222  cusgr3cyclex  35252  resconn  35362  cvmlift2lem9  35427  rdgprc0  35907  bj-snsetex  37080  bj-tagex  37104  bj-0int  37218  poimirlem30  37763  ftc1anclem3  37808  ftc1anclem6  37811  rrnheibor  37950  rngo1cl  38052  isdrngo1  38069  dfcoeleqvrels  38790  islpln2ah  39721  lhpocnel2  40191  cdlemg31b0N  40866  cdlemg31b0a  40867  cdlemh  40989  cdlemk19w  41144  aks4d1lem1  42228  sticksstones4  42315  mzpclval  42882  wopprc  43187  dfac21  43223  uniel  43374  sucomisnotcard  43701  binomcxplemdvsum  44512  binomcxp  44514  mccl  45760  fprodcn  45762  stoweidlem17  46177  fourierdlem89  46355  fourierdlem90  46356  fourierdlem91  46357  fourierdlem100  46366  omeiunltfirp  46679  hoidmvlelem5  46759  issmf  46888  issmff  46894  smflimlem4  46934  smflim  46937  smflim2  46966  smflimsuplem1  46980  smflimsuplem8  46987  smflimsup  46988  chnerlem1  47042  aiotaexb  47251  aiotavb  47252  aovvdm  47347  aovvfunressn  47349  aovrcl  47351  aovvoveq  47354  aov0nbovbi  47357  fnotaovb  47360  mod2addne  47526  prmdvdsfmtnof1lem1  47746  341fppr2  47896  9fppr8  47899  clnbupgrel  47996  grtriproplem  48101  grtrif1o  48104  grtriclwlk3  48107  usgrgrtrirex  48112  isubgr3stgrlem7  48134  grlimprclnbgr  48158  grlimprclnbgrvtx  48161  usgrexmpl1  48184  usgrexmpl2  48189  gpgvtxedg0  48225  gpgvtxedg1  48226  gpgedg2ov  48228  gpgedg2iv  48229  gpgprismgr4cycllem11  48267  pgnbgreunbgrlem1  48275  pgnbgreunbgrlem2lem3  48278  pgnbgreunbgrlem2  48279  pgnbgreunbgrlem4  48281  pgnbgreunbgrlem5  48285  pgnbgreunbgr  48287  pgn4cyclex  48288  zlmodzxzldeplem3  48664  itscnhlinecirc02p  48947  fonex  49028  idemb  49320