Theorem eleq2i 2271

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

Syntax hints:   ↔ wb 105   = wceq 1372   ∈ wcel 2175

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 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532  ax-17 1548  ax-ial 1556  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-cleq 2197  df-clel 2200

This theorem is referenced by:  eleq12i  2272  eleqtri  2279  eleq2s  2299  hbxfreq  2311  abeq2i  2315  abeq1i  2316  nfceqi  2343  raleqbii  2517  rexeqbii  2518  rabeq2i  2768  elab2g  2919  elrabf  2926  elrab3t  2927  elrab2  2931  cbvsbcw  3025  cbvsbc  3026  csbcow  3103  elin2  3360  dfnul2  3461  noel  3463  rabn0m  3487  rabeq0  3489  eltpg  3677  tpid3g  3747  oprcl  3842  elunirab  3862  elintrab  3896  exss  4270  elop  4274  opm  4277  brabsb  4306  brabga  4309  pofun  4358  elsuci  4449  elsucg  4450  elsuc2g  4451  ordsucim  4547  peano2  4642  elxp  4691  brab2a  4727  brab2ga  4749  elco  4843  elcnv  4854  dmmrnm  4896  elrnmptg  4929  opelres  4963  rninxp  5125  eliota  5258  funco  5310  elfv  5573  nfvres  5609  fvopab3g  5651  fvmptssdm  5663  fmptco  5745  funfvima  5815  fliftel  5861  acexmidlema  5934  acexmidlemb  5935  acexmidlem2  5940  eloprabga  6031  elrnmpo  6058  ovid  6061  offval  6165  xporderlem  6316  brtpos2  6336  issmo  6373  smores3  6378  tfrlem7  6402  tfrlem9  6404  tfr0dm  6407  tfri2  6451  rdgon  6471  freccllem  6487  frecfcllem  6489  frecsuclem  6491  el1o  6522  dif1o  6523  nnsucuniel  6580  elecg  6659  brecop  6711  erovlem  6713  oviec  6727  mapsncnv  6781  mptelixpg  6820  isfi  6851  enssdom  6852  map1  6903  xpcomco  6920  exmidpw  7004  exmidpweq  7005  tpfidceq  7026  fnfi  7037  fidcenumlemrks  7054  fidcenumlemrk  7055  djulclb  7156  eldju  7169  eldju2ndl  7173  eldju2ndr  7174  ctssdccl  7212  pw1nel3  7342  sucpw1nel3  7344  elni  7420  nlt1pig  7453  0nnq  7476  dfmq0qs  7541  dfplq0qs  7542  nqnq0  7553  elinp  7586  0npr  7595  ltdfpr  7618  nqprl  7663  nqpru  7664  addnqprlemfl  7671  addnqprlemfu  7672  mulnqprlemfl  7687  mulnqprlemfu  7688  cauappcvgprlemladdru  7768  suplocexprlemell  7825  addsrpr  7857  mulsrpr  7858  opelcn  7938  opelreal  7939  elreal  7940  elreal2  7942  0ncn  7943  addcnsr  7946  mulcnsr  7947  addvalex  7956  peano1nnnn  7964  peano2nnnn  7965  xrlenlt  8136  1nn  9046  peano2nn  9047  elnn0  9296  elnnne0  9308  un0addcl  9327  un0mulcl  9328  elxnn0  9359  uztrn2  9665  elnnuz  9684  elnn0uz  9685  elq  9742  elxr  9897  elfzm1b  10219  fz01or  10232  infssuzex  10374  frecfzennn  10569  inftonninf  10585  seqf  10607  ser0  10676  ser0f  10677  hashinfom  10921  iswrd  10994  clim2ser  11590  clim2ser2  11591  isermulc2  11593  iserle  11595  climserle  11598  fsum3cvg3  11649  isumclim3  11676  isumadd  11684  sumsplitdc  11685  iserabs  11728  cvgcmpub  11729  isumshft  11743  isumsplit  11744  isumlessdc  11749  cvgratz  11785  cvgratgt0  11786  clim2prod  11792  clim2divap  11793  prodf1  11795  zproddc  11832  prodsnf  11845  divides  12042  dvdsflip  12104  nninfctlemfo  12303  ialgrlemconst  12307  prm23lt5  12528  4sqlem2  12654  4sqlem12  12667  ennnfonelemjn  12715  ennnfonelem1  12720  ennnfonelemdm  12733  basmex  12833  ghmeqker  13549  isrhm  13862  rrgmex  13965  lssmex  14059  lidlmex  14179  2idlmex  14205  df2idl2  14213  2idlss  14218  psrbagf  14374  istps  14446  lmss  14660  txuni2  14670  dvply1  15179  sinq34lt0t  15245  lgsdir2lem2  15448  gausslemma2dlem1a  15477  lgsquadlem1  15496  lgsquadlem2  15497  2sqlem1  15533  bdceq  15711  bj-nntrans  15820  bj-nnelirr  15822  ss1oel2o  15861  trilpolemisumle  15910