Theorem eleq1i 2827

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 2824	. 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 2708

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

This theorem is referenced by:  eleq12i  2829  eqeltri  2832  eqneltri  2855  intexrab  5288  abssexg  5324  rmorabex  5412  otelxp  5675  xpsspw  5765  dfse2  6065  dfse3  6300  ordtri3or  6355  fressnfv  7114  fnotovb  7419  ovmpos  7515  abnex  7711  sucexb  7758  f1stres  7966  f2ndres  7967  elxp6  7976  ottpos  8186  dftpos4  8195  tfr2b  8335  tz7.48-3  8383  unfi  9105  difinf  9221  fiint  9237  infssuni  9256  fsuppunbi  9302  r1pwALT  9770  djuexb  9833  alephprc  10021  fin1a2lem12  10333  axcclem  10379  zorn2lem4  10421  zornn0g  10427  grothomex  10752  grothprimlem  10756  addclprlem2  10940  axicn  11073  0mnnnnn0  12469  fcdmnn0fsupp  12495  pfxccatin12lem3  14694  pfxccat3  14696  swrdccat  14697  pfxccat3a  14700  swrdccat3blem  14701  swrdccat3b  14702  harmonic  15824  nprmi  16658  issubmgm  18670  issubm  18771  idresefmnd  18867  mulgfval  19045  oppgsubm  19337  idrespermg  19386  issrg  20169  srgfcl  20177  subrngrng  20527  opprsubrng  20536  rhmimasubrng  20543  cntzsubrng  20544  opprsubrg  20570  rngridlmcl  21215  isridlrng  21217  isridl  21250  resubdrg  21588  cpmidpmat  22838  kgencn  23521  kgencn2  23522  txdis1cn  23600  qtopres  23663  qtopcn  23679  cfinfil  23858  tgphaus  24082  xmeterval  24397  blval2  24527  metuel2  24530  iscvsp  25095  zclmncvs  25115  caucfil  25250  resscdrg  25325  finiunmbl  25511  iblre  25761  dvfsumlem2  25994  logno1  26600  rlimcnp2  26930  ppi2i  27132  gausslemma2dlem1a  27328  2lgslem4  27369  noxp1o  27627  usgrexmpl  29332  usgredgffibi  29393  nbupgrel  29414  nbuhgr2vtx1edgb  29421  nbusgreledg  29422  nbusgrf1o0  29438  nb3grpr  29451  nb3grpr2  29452  nb3gr2nb  29453  cusgrsizeinds  29521  cusgrfi  29527  finsumvtxdg2size  29619  wlkp1lem1  29740  wlkp1lem7  29746  wlkp1lem8  29747  wwlks2onsym  30028  rusgrnumwwlks  30045  clwwlknclwwlkdifnum  30050  clwwlknonfin  30164  clwwlknonex2  30179  umgr3cyclex  30253  eupthp1  30286  eupth2eucrct  30287  frcond3  30339  frgr3v  30345  3vfriswmgr  30348  1to3vfriendship  30351  2pthfrgrrn  30352  3cyclfrgrrn1  30355  4cycl2v2nb  30359  frgrnbnb  30363  frgrncvvdeqlem3  30371  frgrncvvdeqlem6  30374  frgrhash2wsp  30402  fusgr2wsp2nb  30404  numclwwlk1  30431  avril1  30533  n0lplig  30554  hhph  31249  nonbooli  31722  pjss2i  31751  atssma  32449  isrrext  34144  hasheuni  34229  dmvlsiga  34273  measiuns  34361  eulerpartlemmf  34519  fissorduni  35233  fineqvrep  35258  onvf1odlem2  35286  onvf1odlem4  35288  cusgr3cyclex  35318  resconn  35428  cvmlift2lem9  35493  rdgprc0  35973  bj-snsetex  37270  bj-tagex  37294  bj-0int  37413  poimirlem30  37971  ftc1anclem3  38016  ftc1anclem6  38019  rrnheibor  38158  rngo1cl  38260  isdrngo1  38277  dfcoeleqvrels  39026  rnqmapeleldisjsim  39183  islpln2ah  39995  lhpocnel2  40465  cdlemg31b0N  41140  cdlemg31b0a  41141  cdlemh  41263  cdlemk19w  41418  aks4d1lem1  42501  sticksstones4  42588  mzpclval  43157  wopprc  43458  dfac21  43494  uniel  43645  sucomisnotcard  43971  binomcxplemdvsum  44782  binomcxp  44784  mccl  46028  fprodcn  46030  stoweidlem17  46445  fourierdlem89  46623  fourierdlem90  46624  fourierdlem91  46625  fourierdlem100  46634  omeiunltfirp  46947  hoidmvlelem5  47027  issmf  47156  issmff  47162  smflimlem4  47202  smflim  47205  smflim2  47234  smflimsuplem1  47248  smflimsuplem8  47255  smflimsup  47256  chnerlem1  47312  aiotaexb  47537  aiotavb  47538  aovvdm  47633  aovvfunressn  47635  aovrcl  47637  aovvoveq  47640  aov0nbovbi  47643  fnotaovb  47646  mod2addne  47818  prmdvdsfmtnof1lem1  48047  341fppr2  48210  9fppr8  48213  clnbupgrel  48310  grtriproplem  48415  grtrif1o  48418  grtriclwlk3  48421  usgrgrtrirex  48426  isubgr3stgrlem7  48448  grlimprclnbgr  48472  grlimprclnbgrvtx  48475  usgrexmpl1  48498  usgrexmpl2  48503  gpgvtxedg0  48539  gpgvtxedg1  48540  gpgedg2ov  48542  gpgedg2iv  48543  gpgprismgr4cycllem11  48581  pgnbgreunbgrlem1  48589  pgnbgreunbgrlem2lem3  48592  pgnbgreunbgrlem2  48593  pgnbgreunbgrlem4  48595  pgnbgreunbgrlem5  48599  pgnbgreunbgr  48601  pgn4cyclex  48602  zlmodzxzldeplem3  48978  itscnhlinecirc02p  49261  fonex  49342  idemb  49634