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  11619  clim2ser2  11620  isermulc2  11622  iserle  11624  climserle  11627  fsum3cvg3  11678  isumclim3  11705  isumadd  11713  sumsplitdc  11714  iserabs  11757  cvgcmpub  11758  isumshft  11772  isumsplit  11773  isumlessdc  11778  cvgratz  11814  cvgratgt0  11815  clim2prod  11821  clim2divap  11822  prodf1  11824  zproddc  11861  prodsnf  11874  divides  12071  dvdsflip  12133  nninfctlemfo  12332  ialgrlemconst  12336  prm23lt5  12557  4sqlem2  12683  4sqlem12  12696  ennnfonelemjn  12744  ennnfonelem1  12749  ennnfonelemdm  12762  basmex  12862  ghmeqker  13578  isrhm  13891  rrgmex  13994  lssmex  14088  lidlmex  14208  2idlmex  14234  df2idl2  14242  2idlss  14247  psrbagf  14403  istps  14475  lmss  14689  txuni2  14699  dvply1  15208  sinq34lt0t  15274  lgsdir2lem2  15477  gausslemma2dlem1a  15506  lgsquadlem1  15525  lgsquadlem2  15526  2sqlem1  15562  bdceq  15740  bj-nntrans  15849  bj-nnelirr  15851  ss1oel2o  15890  trilpolemisumle  15939