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  4369  elop  4373  opm  4376  brabsb  4405  brabga  4408  pofun  4459  elsuci  4550  elsucg  4551  elsuc2g  4552  ordsucim  4649  peano2  4744  elxp  4793  brab2a  4830  brab2ga  4852  elco  4948  elcnv  4959  dmmrnm  5003  elrnmptg  5036  opelres  5070  rninxp  5234  eliota  5368  funco  5420  elfv  5696  nfvres  5735  fvopab3g  5781  fvmptssdm  5793  fmptco  5877  funfvima  5953  fliftel  6002  acexmidlema  6079  acexmidlemb  6080  acexmidlem2  6085  eloprabga  6178  elrnmpo  6205  ovid  6208  offval  6314  xporderlem  6471  brtpos2  6526  issmo  6563  smores3  6568  tfrlem7  6592  tfrlem9  6594  tfr0dm  6597  tfri2  6641  rdgon  6661  freccllem  6677  frecfcllem  6679  frecsuclem  6681  el1o  6714  dif1o  6715  nnsucuniel  6772  elecg  6851  brecop  6903  erovlem  6905  oviec  6919  mapsncnv  6981  mptelixpg  7020  isfi  7051  enssdom  7052  map1  7105  xpcomco  7128  exmidpw  7219  exmidpweq  7220  tpfidceq  7241  fnfi  7254  fidcenumlemrks  7275  fidcenumlemrk  7276  djulclb  7401  eldju  7414  eldju2ndl  7418  eldju2ndr  7419  ctssdccl  7457  pw1nel3  7596  sucpw1nel3  7598  elni  7681  nlt1pig  7714  0nnq  7737  dfmq0qs  7802  dfplq0qs  7803  nqnq0  7814  elinp  7847  0npr  7856  ltdfpr  7879  nqprl  7924  nqpru  7925  addnqprlemfl  7932  addnqprlemfu  7933  mulnqprlemfl  7948  mulnqprlemfu  7949  cauappcvgprlemladdru  8029  suplocexprlemell  8086  addsrpr  8118  mulsrpr  8119  opelcn  8199  opelreal  8200  elreal  8201  elreal2  8203  0ncn  8204  addcnsr  8207  mulcnsr  8208  addvalex  8217  peano1nnnn  8225  peano2nnnn  8226  xrlenlt  8396  1nn  9324  peano2nn  9325  elnn0  9576  elnnne0  9588  un0addcl  9607  un0mulcl  9608  elxnn0  9643  uztrn2  9956  elnnuz  9975  elnn0uz  9976  elq  10038  elxr  10195  elfzm1b  10522  fz01or  10535  infssuzex  10683  infssfzcldc  10686  infssfzledc  10687  frecfzennn  10884  inftonninf  10900  seqf  10922  ser0  10991  ser0f  10992  hashinfom  11239  iswrd  11328  pfxccatpfx1  11530  clim2ser  12128  clim2ser2  12129  isermulc2  12131  iserle  12133  climserle  12136  fsum3cvg3  12188  isumclim3  12215  isumadd  12223  sumsplitdc  12224  iserabs  12267  cvgcmpub  12268  isumshft  12282  isumsplit  12283  isumlessdc  12288  cvgratz  12324  cvgratgt0  12325  clim2prod  12331  clim2divap  12332  prodf1  12334  zproddc  12371  prodsnf  12384  divides  12581  dvdsflip  12643  nninfctlemfo  12842  ialgrlemconst  12846  prm23lt5  13071  4sqlem2  13197  4sqlem12  13210  ballotfilemfrcn0  13331  ballotfilem7  13337  ennnfonelemjn  13351  ennnfonelem1  13356  ennnfonelemdm  13369  basmex  13470  ghmeqker  14133  elcntr  14163  cntri  14165  cntzsgrpcl  14167  idjusnfi  14270  opprringb  14495  isrhm  14574  rrgmex  14678  lssmex  14801  lidlmex  14921  2idlmex  14947  df2idl2  14955  2idlss  14960  psrbagf  15163  istps  15258  lmss  15472  txuni2  15482  dvply1  15991  sinq34lt0t  16058  logfac  16126  ppiublem1  16291  lgsdir2lem2  16353  gausslemma2dlem1a  16382  lgsquadlem1  16401  lgsquadlem2  16402  2sqlem1  16438  isuhgrm  16517  isushgrm  16518  isupgren  16541  isumgren  16551  umgredg  16591  umgrpredgv  16593  umgredgne  16596  umgredgnlp  16598  isuspgren  16603  isusgren  16604  ausgrusgrien  16617  usgredgppren  16643  edgssv2en  16645  uspgredg2vlem  16666  uspgredg2v  16667  ushgredgedg  16672  ushgredgedgloop  16674  griedg0ssusgr  16697  uhgrissubgr  16707  subumgredg2en  16717  uhgrspansubgrlem  16722  vtxedgfi  16735  vtxlpfi  16736  vtxdg0v  16740  wlk1walkdom  16805  clwwlkccatlem  16846  clwwlknnn  16858  clwwlknon2x  16881  bdceq  17073  bj-nntrans  17182  bj-nnelirr  17184  ss1oel2o  17222  wexmiddifxylem  17250  idjudju  17252  trilpolemisumle  17294