Theorem eleq2i 2296

Description: Inference from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
eleq1i.1	|- A = B

Assertion

Ref	Expression
eleq2i	|- ( C e. A <-> C e. B )

Proof of Theorem eleq2i

Step	Hyp	Ref	Expression
1		eleq1i.1	. 2 |- A = B
2		eleq2 2293	. 2 |- ( A = B -> ( C e. A <-> C e. B ) )
3	1, 2	ax-mp 5	1 |- ( C e. A <-> C e. B )

Syntax hints:   <-> wb 105   = wceq 1395   e. wcel 2200

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  eleq12i  2297  eleqtri  2304  eleq2s  2324  hbxfreq  2336  abeq2i  2340  abeq1i  2341  nfceqi  2368  raleqbii  2542  rexeqbii  2543  rabeq2i  2796  elab2g  2950  elrabf  2957  elrab3t  2958  elrab2  2962  cbvsbcw  3056  cbvsbc  3057  csbcow  3135  elin2  3392  dfnul2  3493  noel  3495  rabn0m  3519  rabeq0  3521  eltpg  3711  tpid3g  3782  oprcl  3881  elunirab  3901  elintrab  3935  exss  4313  elop  4317  opm  4320  brabsb  4349  brabga  4352  pofun  4403  elsuci  4494  elsucg  4495  elsuc2g  4496  ordsucim  4592  peano2  4687  elxp  4736  brab2a  4772  brab2ga  4794  elco  4888  elcnv  4899  dmmrnm  4943  elrnmptg  4976  opelres  5010  rninxp  5172  eliota  5306  funco  5358  elfv  5625  nfvres  5663  fvopab3g  5707  fvmptssdm  5719  fmptco  5801  funfvima  5871  fliftel  5917  acexmidlema  5992  acexmidlemb  5993  acexmidlem2  5998  eloprabga  6091  elrnmpo  6118  ovid  6121  offval  6226  xporderlem  6377  brtpos2  6397  issmo  6434  smores3  6439  tfrlem7  6463  tfrlem9  6465  tfr0dm  6468  tfri2  6512  rdgon  6532  freccllem  6548  frecfcllem  6550  frecsuclem  6552  el1o  6583  dif1o  6584  nnsucuniel  6641  elecg  6720  brecop  6772  erovlem  6774  oviec  6788  mapsncnv  6842  mptelixpg  6881  isfi  6912  enssdom  6913  map1  6965  xpcomco  6985  exmidpw  7070  exmidpweq  7071  tpfidceq  7092  fnfi  7103  fidcenumlemrks  7120  fidcenumlemrk  7121  djulclb  7222  eldju  7235  eldju2ndl  7239  eldju2ndr  7240  ctssdccl  7278  pw1nel3  7416  sucpw1nel3  7418  elni  7495  nlt1pig  7528  0nnq  7551  dfmq0qs  7616  dfplq0qs  7617  nqnq0  7628  elinp  7661  0npr  7670  ltdfpr  7693  nqprl  7738  nqpru  7739  addnqprlemfl  7746  addnqprlemfu  7747  mulnqprlemfl  7762  mulnqprlemfu  7763  cauappcvgprlemladdru  7843  suplocexprlemell  7900  addsrpr  7932  mulsrpr  7933  opelcn  8013  opelreal  8014  elreal  8015  elreal2  8017  0ncn  8018  addcnsr  8021  mulcnsr  8022  addvalex  8031  peano1nnnn  8039  peano2nnnn  8040  xrlenlt  8211  1nn  9121  peano2nn  9122  elnn0  9371  elnnne0  9383  un0addcl  9402  un0mulcl  9403  elxnn0  9434  uztrn2  9740  elnnuz  9759  elnn0uz  9760  elq  9817  elxr  9972  elfzm1b  10294  fz01or  10307  infssuzex  10453  frecfzennn  10648  inftonninf  10664  seqf  10686  ser0  10755  ser0f  10756  hashinfom  11000  iswrd  11073  pfxccatpfx1  11268  clim2ser  11848  clim2ser2  11849  isermulc2  11851  iserle  11853  climserle  11856  fsum3cvg3  11907  isumclim3  11934  isumadd  11942  sumsplitdc  11943  iserabs  11986  cvgcmpub  11987  isumshft  12001  isumsplit  12002  isumlessdc  12007  cvgratz  12043  cvgratgt0  12044  clim2prod  12050  clim2divap  12051  prodf1  12053  zproddc  12090  prodsnf  12103  divides  12300  dvdsflip  12362  nninfctlemfo  12561  ialgrlemconst  12565  prm23lt5  12786  4sqlem2  12912  4sqlem12  12925  ennnfonelemjn  12973  ennnfonelem1  12978  ennnfonelemdm  12991  basmex  13092  ghmeqker  13808  isrhm  14122  rrgmex  14225  lssmex  14319  lidlmex  14439  2idlmex  14465  df2idl2  14473  2idlss  14478  psrbagf  14634  istps  14706  lmss  14920  txuni2  14930  dvply1  15439  sinq34lt0t  15505  lgsdir2lem2  15708  gausslemma2dlem1a  15737  lgsquadlem1  15756  lgsquadlem2  15757  2sqlem1  15793  isuhgrm  15871  isushgrm  15872  isupgren  15895  isumgren  15905  umgredg  15943  umgrpredgv  15945  umgredgne  15948  umgredgnlp  15950  isuspgren  15955  isusgren  15956  ausgrusgrien  15969  usgredgppren  15995  edgssv2en  15997  uspgredg2vlem  16018  uspgredg2v  16019  ushgredgedg  16024  ushgredgedgloop  16026  wlk1walkdom  16070  bdceq  16205  bj-nntrans  16314  bj-nnelirr  16316  ss1oel2o  16355  trilpolemisumle  16406