Theorem eleq2i 2305

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 2302	. 2 |- ( A = B -> ( C e. A <-> C e. B ) )
3	1, 2	ax-mp 5	1 |- ( C e. A <-> C e. B )

This proof depends on syntax axioms:   <-> wb 105   = wceq 1402   e. 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  6982  mptelixpg  7021  isfi  7052  enssdom  7053  map1  7106  xpcomco  7129  exmidpw  7220  exmidpweq  7221  tpfidceq  7242  fnfi  7255  fidcenumlemrks  7276  fidcenumlemrk  7277  djulclb  7402  eldju  7415  eldju2ndl  7419  eldju2ndr  7420  ctssdccl  7458  pw1nel3  7597  sucpw1nel3  7599  elni  7682  nlt1pig  7715  0nnq  7738  dfmq0qs  7803  dfplq0qs  7804  nqnq0  7815  elinp  7848  0npr  7857  ltdfpr  7880  nqprl  7925  nqpru  7926  addnqprlemfl  7933  addnqprlemfu  7934  mulnqprlemfl  7949  mulnqprlemfu  7950  cauappcvgprlemladdru  8030  suplocexprlemell  8087  addsrpr  8119  mulsrpr  8120  opelcn  8200  opelreal  8201  elreal  8202  elreal2  8204  0ncn  8205  addcnsr  8208  mulcnsr  8209  addvalex  8218  peano1nnnn  8226  peano2nnnn  8227  xrlenlt  8397  1nn  9325  peano2nn  9326  elnn0  9577  elnnne0  9589  un0addcl  9608  un0mulcl  9609  elxnn0  9644  uztrn2  9957  elnnuz  9976  elnn0uz  9977  elq  10039  elxr  10196  elfzm1b  10523  fz01or  10536  infssuzex  10684  infssfzcldc  10687  infssfzledc  10688  frecfzennn  10885  inftonninf  10901  seqf  10923  ser0  10992  ser0f  10993  hashinfom  11240  iswrd  11329  pfxccatpfx1  11531  clim2ser  12129  clim2ser2  12130  isermulc2  12132  iserle  12134  climserle  12137  fsum3cvg3  12189  isumclim3  12216  isumadd  12224  sumsplitdc  12225  iserabs  12268  cvgcmpub  12269  isumshft  12283  isumsplit  12284  isumlessdc  12289  cvgratz  12325  cvgratgt0  12326  clim2prod  12332  clim2divap  12333  prodf1  12335  zproddc  12372  prodsnf  12385  divides  12582  dvdsflip  12644  nninfctlemfo  12843  ialgrlemconst  12847  prm23lt5  13072  4sqlem2  13198  4sqlem12  13211  ballotfilemfrcn0  13332  ballotfilem7  13338  ennnfonelemjn  13352  ennnfonelem1  13357  ennnfonelemdm  13370  basmex  13471  ghmeqker  14134  elcntr  14164  cntri  14166  cntzsgrpcl  14168  idjusnfi  14271  opprringb  14496  isrhm  14575  rrgmex  14679  lssmex  14802  lidlmex  14922  2idlmex  14948  df2idl2  14956  2idlss  14961  psrbagf  15166  istps  15270  lmss  15484  txuni2  15494  dvply1  16003  sinq34lt0t  16070  logfac  16138  ppiublem1  16303  lgsdir2lem2  16365  gausslemma2dlem1a  16394  lgsquadlem1  16413  lgsquadlem2  16414  2sqlem1  16450  isuhgrm  16529  isushgrm  16530  isupgren  16553  isumgren  16563  umgredg  16603  umgrpredgv  16605  umgredgne  16608  umgredgnlp  16610  isuspgren  16615  isusgren  16616  ausgrusgrien  16629  usgredgppren  16655  edgssv2en  16657  uspgredg2vlem  16678  uspgredg2v  16679  ushgredgedg  16684  ushgredgedgloop  16686  griedg0ssusgr  16709  uhgrissubgr  16719  subumgredg2en  16729  uhgrspansubgrlem  16734  vtxedgfi  16747  vtxlpfi  16748  vtxdg0v  16752  wlk1walkdom  16817  clwwlkccatlem  16858  clwwlknnn  16870  clwwlknon2x  16893  bdceq  17085  bj-nntrans  17194  bj-nnelirr  17196  ss1oel2o  17234  wexmiddifxylem  17262  idjudju  17264  trilpolemisumle  17306