Theorem eleq2i 2305

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

This proof depends on syntax axioms:   ↔ wb 105   = wceq 1402   ∈ wcel 2209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  eleq12i  2306  eleqtri  2313  eleq2s  2333  hbxfreq  2345  abeq2i  2349  abeq1i  2350  nfceqi  2388  raleqbii  2562  rexeqbii  2563  reqabi  2728  rabeq2i  2818  elab2g  2973  elrabf  2980  elrab3t  2981  elrab2  2985  cbvsbcw  3079  cbvsbc  3080  csbcow  3158  elin2  3417  noel  3525  rabn0m  3549  rabeq0  3552  eltpg  3754  tpid3g  3828  oprcl  3928  elunirab  3948  elintrab  3982  exss  4367  elop  4371  opm  4374  brabsb  4403  brabga  4406  pofun  4457  elsuci  4548  elsucg  4549  elsuc2g  4550  ordsucim  4647  peano2  4742  elxp  4791  brab2a  4828  brab2ga  4850  elco  4946  elcnv  4957  dmmrnm  5001  elrnmptg  5034  opelres  5068  rninxp  5231  eliota  5365  funco  5417  elfv  5693  nfvres  5732  fvopab3g  5778  fvmptssdm  5790  fmptco  5874  funfvima  5950  fliftel  5999  acexmidlema  6076  acexmidlemb  6077  acexmidlem2  6082  eloprabga  6175  elrnmpo  6202  ovid  6205  offval  6310  xporderlem  6467  brtpos2  6522  issmo  6559  smores3  6564  tfrlem7  6588  tfrlem9  6590  tfr0dm  6593  tfri2  6637  rdgon  6657  freccllem  6673  frecfcllem  6675  frecsuclem  6677  el1o  6710  dif1o  6711  nnsucuniel  6768  elecg  6847  brecop  6899  erovlem  6901  oviec  6915  mapsncnv  6977  mptelixpg  7016  isfi  7047  enssdom  7048  map1  7101  xpcomco  7124  exmidpw  7215  exmidpweq  7216  tpfidceq  7237  fnfi  7250  fidcenumlemrks  7270  fidcenumlemrk  7271  djulclb  7396  eldju  7409  eldju2ndl  7413  eldju2ndr  7414  ctssdccl  7452  pw1nel3  7591  sucpw1nel3  7593  elni  7676  nlt1pig  7709  0nnq  7732  dfmq0qs  7797  dfplq0qs  7798  nqnq0  7809  elinp  7842  0npr  7851  ltdfpr  7874  nqprl  7919  nqpru  7920  addnqprlemfl  7927  addnqprlemfu  7928  mulnqprlemfl  7943  mulnqprlemfu  7944  cauappcvgprlemladdru  8024  suplocexprlemell  8081  addsrpr  8113  mulsrpr  8114  opelcn  8194  opelreal  8195  elreal  8196  elreal2  8198  0ncn  8199  addcnsr  8202  mulcnsr  8203  addvalex  8212  peano1nnnn  8220  peano2nnnn  8221  xrlenlt  8391  1nn  9318  peano2nn  9319  elnn0  9570  elnnne0  9582  un0addcl  9601  un0mulcl  9602  elxnn0  9637  uztrn2  9950  elnnuz  9969  elnn0uz  9970  elq  10032  elxr  10189  elfzm1b  10516  fz01or  10529  infssuzex  10677  infssfzcldc  10680  infssfzledc  10681  frecfzennn  10878  inftonninf  10894  seqf  10916  ser0  10985  ser0f  10986  hashinfom  11233  iswrd  11322  pfxccatpfx1  11524  clim2ser  12122  clim2ser2  12123  isermulc2  12125  iserle  12127  climserle  12130  fsum3cvg3  12182  isumclim3  12209  isumadd  12217  sumsplitdc  12218  iserabs  12261  cvgcmpub  12262  isumshft  12276  isumsplit  12277  isumlessdc  12282  cvgratz  12318  cvgratgt0  12319  clim2prod  12325  clim2divap  12326  prodf1  12328  zproddc  12365  prodsnf  12378  divides  12575  dvdsflip  12637  nninfctlemfo  12836  ialgrlemconst  12840  prm23lt5  13065  4sqlem2  13191  4sqlem12  13204  ballotfilemfrcn0  13325  ballotfilem7  13331  ennnfonelemjn  13345  ennnfonelem1  13350  ennnfonelemdm  13363  basmex  13464  ghmeqker  14127  elcntr  14157  cntri  14159  cntzsgrpcl  14161  opprringb  14470  isrhm  14549  rrgmex  14653  lssmex  14776  lidlmex  14896  2idlmex  14922  df2idl2  14930  2idlss  14935  psrbagf  15138  istps  15224  lmss  15438  txuni2  15448  dvply1  15957  sinq34lt0t  16024  logfac  16090  ppiublem1  16252  lgsdir2lem2  16314  gausslemma2dlem1a  16343  lgsquadlem1  16362  lgsquadlem2  16363  2sqlem1  16399  isuhgrm  16478  isushgrm  16479  isupgren  16502  isumgren  16512  umgredg  16552  umgrpredgv  16554  umgredgne  16557  umgredgnlp  16559  isuspgren  16564  isusgren  16565  ausgrusgrien  16578  usgredgppren  16604  edgssv2en  16606  uspgredg2vlem  16627  uspgredg2v  16628  ushgredgedg  16633  ushgredgedgloop  16635  griedg0ssusgr  16658  uhgrissubgr  16668  subumgredg2en  16678  uhgrspansubgrlem  16683  vtxedgfi  16696  vtxlpfi  16697  vtxdg0v  16701  wlk1walkdom  16766  clwwlkccatlem  16807  clwwlknnn  16819  clwwlknon2x  16842  bdceq  17034  bj-nntrans  17143  bj-nnelirr  17145  ss1oel2o  17183  wexmiddifxylem  17211  trilpolemisumle  17254