Theorem eleq2i 2298

Description: Inference from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
eleq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
eleq2i	⊢ (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵)

Proof of Theorem eleq2i

Step	Hyp	Ref	Expression
1		eleq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		eleq2 2295	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵)

Syntax hints:   ↔ wb 105   = wceq 1398   ∈ wcel 2202

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227

This theorem is referenced by:  eleq12i  2299  eleqtri  2306  eleq2s  2326  hbxfreq  2338  abeq2i  2342  abeq1i  2343  nfceqi  2371  raleqbii  2545  rexeqbii  2546  rabeq2i  2800  elab2g  2954  elrabf  2961  elrab3t  2962  elrab2  2966  cbvsbcw  3060  cbvsbc  3061  csbcow  3139  elin2  3397  dfnul2  3498  noel  3500  rabn0m  3524  rabeq0  3526  eltpg  3718  tpid3g  3791  oprcl  3891  elunirab  3911  elintrab  3945  exss  4325  elop  4329  opm  4332  brabsb  4361  brabga  4364  pofun  4415  elsuci  4506  elsucg  4507  elsuc2g  4508  ordsucim  4604  peano2  4699  elxp  4748  brab2a  4785  brab2ga  4807  elco  4902  elcnv  4913  dmmrnm  4957  elrnmptg  4990  opelres  5024  rninxp  5187  eliota  5321  funco  5373  elfv  5646  nfvres  5684  fvopab3g  5728  fvmptssdm  5740  fmptco  5821  funfvima  5896  fliftel  5944  acexmidlema  6019  acexmidlemb  6020  acexmidlem2  6025  eloprabga  6118  elrnmpo  6145  ovid  6148  offval  6252  xporderlem  6405  brtpos2  6460  issmo  6497  smores3  6502  tfrlem7  6526  tfrlem9  6528  tfr0dm  6531  tfri2  6575  rdgon  6595  freccllem  6611  frecfcllem  6613  frecsuclem  6615  el1o  6648  dif1o  6649  nnsucuniel  6706  elecg  6785  brecop  6837  erovlem  6839  oviec  6853  mapsncnv  6907  mptelixpg  6946  isfi  6977  enssdom  6978  map1  7030  xpcomco  7053  exmidpw  7143  exmidpweq  7144  tpfidceq  7165  fnfi  7178  fidcenumlemrks  7195  fidcenumlemrk  7196  djulclb  7297  eldju  7310  eldju2ndl  7314  eldju2ndr  7315  ctssdccl  7353  pw1nel3  7492  sucpw1nel3  7494  elni  7571  nlt1pig  7604  0nnq  7627  dfmq0qs  7692  dfplq0qs  7693  nqnq0  7704  elinp  7737  0npr  7746  ltdfpr  7769  nqprl  7814  nqpru  7815  addnqprlemfl  7822  addnqprlemfu  7823  mulnqprlemfl  7838  mulnqprlemfu  7839  cauappcvgprlemladdru  7919  suplocexprlemell  7976  addsrpr  8008  mulsrpr  8009  opelcn  8089  opelreal  8090  elreal  8091  elreal2  8093  0ncn  8094  addcnsr  8097  mulcnsr  8098  addvalex  8107  peano1nnnn  8115  peano2nnnn  8116  xrlenlt  8286  1nn  9196  peano2nn  9197  elnn0  9446  elnnne0  9458  un0addcl  9477  un0mulcl  9478  elxnn0  9511  uztrn2  9818  elnnuz  9837  elnn0uz  9838  elq  9900  elxr  10055  elfzm1b  10378  fz01or  10391  infssuzex  10539  frecfzennn  10734  inftonninf  10750  seqf  10772  ser0  10841  ser0f  10842  hashinfom  11086  iswrd  11164  pfxccatpfx1  11366  clim2ser  11960  clim2ser2  11961  isermulc2  11963  iserle  11965  climserle  11968  fsum3cvg3  12020  isumclim3  12047  isumadd  12055  sumsplitdc  12056  iserabs  12099  cvgcmpub  12100  isumshft  12114  isumsplit  12115  isumlessdc  12120  cvgratz  12156  cvgratgt0  12157  clim2prod  12163  clim2divap  12164  prodf1  12166  zproddc  12203  prodsnf  12216  divides  12413  dvdsflip  12475  nninfctlemfo  12674  ialgrlemconst  12678  prm23lt5  12899  4sqlem2  13025  4sqlem12  13038  ennnfonelemjn  13086  ennnfonelem1  13091  ennnfonelemdm  13104  basmex  13205  ghmeqker  13921  isrhm  14236  rrgmex  14339  lssmex  14434  lidlmex  14554  2idlmex  14580  df2idl2  14588  2idlss  14593  psrbagf  14749  istps  14826  lmss  15040  txuni2  15050  dvply1  15559  sinq34lt0t  15625  lgsdir2lem2  15831  gausslemma2dlem1a  15860  lgsquadlem1  15879  lgsquadlem2  15880  2sqlem1  15916  isuhgrm  15995  isushgrm  15996  isupgren  16019  isumgren  16029  umgredg  16069  umgrpredgv  16071  umgredgne  16074  umgredgnlp  16076  isuspgren  16081  isusgren  16082  ausgrusgrien  16095  usgredgppren  16121  edgssv2en  16123  uspgredg2vlem  16144  uspgredg2v  16145  ushgredgedg  16150  ushgredgedgloop  16152  griedg0ssusgr  16175  uhgrissubgr  16185  subumgredg2en  16195  uhgrspansubgrlem  16200  vtxedgfi  16213  vtxlpfi  16214  vtxdg0v  16218  wlk1walkdom  16283  clwwlkccatlem  16324  clwwlknnn  16336  clwwlknon2x  16359  bdceq  16541  bj-nntrans  16650  bj-nnelirr  16652  ss1oel2o  16690  trilpolemisumle  16753