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  5294  abssexg  5329  rmorabex  5415  otelxp  5676  xpsspw  5766  dfse2  6067  dfse3  6302  ordtri3or  6357  fressnfv  7115  fnotovb  7420  ovmpos  7516  abnex  7712  sucexb  7759  f1stres  7967  f2ndres  7968  elxp6  7977  ottpos  8188  dftpos4  8197  tfr2b  8337  tz7.48-3  8385  unfi  9107  difinf  9223  fiint  9239  infssuni  9258  fsuppunbi  9304  r1pwALT  9770  djuexb  9833  alephprc  10021  fin1a2lem12  10333  axcclem  10379  zorn2lem4  10421  zornn0g  10427  grothomex  10752  grothprimlem  10756  addclprlem2  10940  axicn  11073  0mnnnnn0  12445  fcdmnn0fsupp  12471  pfxccatin12lem3  14667  pfxccat3  14669  swrdccat  14670  pfxccat3a  14673  swrdccat3blem  14674  swrdccat3b  14675  harmonic  15794  nprmi  16628  issubmgm  18639  issubm  18740  idresefmnd  18836  mulgfval  19011  oppgsubm  19303  idrespermg  19352  issrg  20135  srgfcl  20143  subrngrng  20495  opprsubrng  20504  rhmimasubrng  20511  cntzsubrng  20512  opprsubrg  20538  rngridlmcl  21184  isridlrng  21186  isridl  21219  resubdrg  21575  cpmidpmat  22829  kgencn  23512  kgencn2  23513  txdis1cn  23591  qtopres  23654  qtopcn  23670  cfinfil  23849  tgphaus  24073  xmeterval  24388  blval2  24518  metuel2  24521  iscvsp  25096  zclmncvs  25116  caucfil  25251  resscdrg  25326  finiunmbl  25513  iblre  25763  dvfsumlem2  26001  logno1  26613  rlimcnp2  26944  ppi2i  27147  gausslemma2dlem1a  27344  2lgslem4  27385  noxp1o  27643  usgrexmpl  29348  usgredgffibi  29409  nbupgrel  29430  nbuhgr2vtx1edgb  29437  nbusgreledg  29438  nbusgrf1o0  29454  nb3grpr  29467  nb3grpr2  29468  nb3gr2nb  29469  cusgrsizeinds  29538  cusgrfi  29544  finsumvtxdg2size  29636  wlkp1lem1  29757  wlkp1lem7  29763  wlkp1lem8  29764  wwlks2onsym  30045  rusgrnumwwlks  30062  clwwlknclwwlkdifnum  30067  clwwlknonfin  30181  clwwlknonex2  30196  umgr3cyclex  30270  eupthp1  30303  eupth2eucrct  30304  frcond3  30356  frgr3v  30362  3vfriswmgr  30365  1to3vfriendship  30368  2pthfrgrrn  30369  3cyclfrgrrn1  30372  4cycl2v2nb  30376  frgrnbnb  30380  frgrncvvdeqlem3  30388  frgrncvvdeqlem6  30391  frgrhash2wsp  30419  fusgr2wsp2nb  30421  numclwwlk1  30448  avril1  30550  n0lplig  30570  hhph  31265  nonbooli  31738  pjss2i  31767  atssma  32465  isrrext  34177  hasheuni  34262  dmvlsiga  34306  measiuns  34394  eulerpartlemmf  34552  fissorduni  35265  fineqvrep  35289  onvf1odlem2  35317  onvf1odlem4  35319  cusgr3cyclex  35349  resconn  35459  cvmlift2lem9  35524  rdgprc0  36004  bj-snsetex  37208  bj-tagex  37232  bj-0int  37351  poimirlem30  37898  ftc1anclem3  37943  ftc1anclem6  37946  rrnheibor  38085  rngo1cl  38187  isdrngo1  38204  dfcoeleqvrels  38953  rnqmapeleldisjsim  39110  islpln2ah  39922  lhpocnel2  40392  cdlemg31b0N  41067  cdlemg31b0a  41068  cdlemh  41190  cdlemk19w  41345  aks4d1lem1  42429  sticksstones4  42516  mzpclval  43079  wopprc  43384  dfac21  43420  uniel  43571  sucomisnotcard  43897  binomcxplemdvsum  44708  binomcxp  44710  mccl  45955  fprodcn  45957  stoweidlem17  46372  fourierdlem89  46550  fourierdlem90  46551  fourierdlem91  46552  fourierdlem100  46561  omeiunltfirp  46874  hoidmvlelem5  46954  issmf  47083  issmff  47089  smflimlem4  47129  smflim  47132  smflim2  47161  smflimsuplem1  47175  smflimsuplem8  47182  smflimsup  47183  chnerlem1  47237  aiotaexb  47446  aiotavb  47447  aovvdm  47542  aovvfunressn  47544  aovrcl  47546  aovvoveq  47549  aov0nbovbi  47552  fnotaovb  47555  mod2addne  47721  prmdvdsfmtnof1lem1  47941  341fppr2  48091  9fppr8  48094  clnbupgrel  48191  grtriproplem  48296  grtrif1o  48299  grtriclwlk3  48302  usgrgrtrirex  48307  isubgr3stgrlem7  48329  grlimprclnbgr  48353  grlimprclnbgrvtx  48356  usgrexmpl1  48379  usgrexmpl2  48384  gpgvtxedg0  48420  gpgvtxedg1  48421  gpgedg2ov  48423  gpgedg2iv  48424  gpgprismgr4cycllem11  48462  pgnbgreunbgrlem1  48470  pgnbgreunbgrlem2lem3  48473  pgnbgreunbgrlem2  48474  pgnbgreunbgrlem4  48476  pgnbgreunbgrlem5  48480  pgnbgreunbgr  48482  pgn4cyclex  48483  zlmodzxzldeplem3  48859  itscnhlinecirc02p  49142  fonex  49223  idemb  49515