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  7395  eldju  7408  eldju2ndl  7412  eldju2ndr  7413  ctssdccl  7451  pw1nel3  7590  sucpw1nel3  7592  elni  7675  nlt1pig  7708  0nnq  7731  dfmq0qs  7796  dfplq0qs  7797  nqnq0  7808  elinp  7841  0npr  7850  ltdfpr  7873  nqprl  7918  nqpru  7919  addnqprlemfl  7926  addnqprlemfu  7927  mulnqprlemfl  7942  mulnqprlemfu  7943  cauappcvgprlemladdru  8023  suplocexprlemell  8080  addsrpr  8112  mulsrpr  8113  opelcn  8193  opelreal  8194  elreal  8195  elreal2  8197  0ncn  8198  addcnsr  8201  mulcnsr  8202  addvalex  8211  peano1nnnn  8219  peano2nnnn  8220  xrlenlt  8390  1nn  9317  peano2nn  9318  elnn0  9569  elnnne0  9581  un0addcl  9600  un0mulcl  9601  elxnn0  9636  uztrn2  9949  elnnuz  9968  elnn0uz  9969  elq  10031  elxr  10188  elfzm1b  10515  fz01or  10528  infssuzex  10676  infssfzcldc  10679  infssfzledc  10680  frecfzennn  10876  inftonninf  10892  seqf  10914  ser0  10983  ser0f  10984  hashinfom  11231  iswrd  11320  pfxccatpfx1  11522  clim2ser  12119  clim2ser2  12120  isermulc2  12122  iserle  12124  climserle  12127  fsum3cvg3  12179  isumclim3  12206  isumadd  12214  sumsplitdc  12215  iserabs  12258  cvgcmpub  12259  isumshft  12273  isumsplit  12274  isumlessdc  12279  cvgratz  12315  cvgratgt0  12316  clim2prod  12322  clim2divap  12323  prodf1  12325  zproddc  12362  prodsnf  12375  divides  12572  dvdsflip  12634  nninfctlemfo  12833  ialgrlemconst  12837  prm23lt5  13062  4sqlem2  13188  4sqlem12  13201  ballotfilemfrcn0  13322  ballotfilem7  13328  ennnfonelemjn  13342  ennnfonelem1  13347  ennnfonelemdm  13360  basmex  13461  ghmeqker  14123  opprringb  14435  isrhm  14514  rrgmex  14618  lssmex  14741  lidlmex  14861  2idlmex  14887  df2idl2  14895  2idlss  14900  psrbagf  15103  istps  15182  lmss  15396  txuni2  15406  dvply1  15915  sinq34lt0t  15982  logfac  16048  ppiublem1  16192  lgsdir2lem2  16246  gausslemma2dlem1a  16275  lgsquadlem1  16294  lgsquadlem2  16295  2sqlem1  16331  isuhgrm  16410  isushgrm  16411  isupgren  16434  isumgren  16444  umgredg  16484  umgrpredgv  16486  umgredgne  16489  umgredgnlp  16491  isuspgren  16496  isusgren  16497  ausgrusgrien  16510  usgredgppren  16536  edgssv2en  16538  uspgredg2vlem  16559  uspgredg2v  16560  ushgredgedg  16565  ushgredgedgloop  16567  griedg0ssusgr  16590  uhgrissubgr  16600  subumgredg2en  16610  uhgrspansubgrlem  16615  vtxedgfi  16628  vtxlpfi  16629  vtxdg0v  16633  wlk1walkdom  16698  clwwlkccatlem  16739  clwwlknnn  16751  clwwlknon2x  16774  bdceq  16966  bj-nntrans  17075  bj-nnelirr  17077  ss1oel2o  17115  wexmiddifxylem  17143  trilpolemisumle  17185