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  4367  elop  4371  opm  4374  brabsb  4403  brabga  4406  pofun  4457  elsuci  4548  elsucg  4549  elsuc2g  4550  ordsucim  4647  peano2  4742  elxp  4791  brab2a  4828  brab2ga  4850  elco  4946  elcnv  4957  dmmrnm  5001  elrnmptg  5034  opelres  5068  rninxp  5231  eliota  5365  funco  5417  elfv  5693  nfvres  5732  fvopab3g  5778  fvmptssdm  5790  fmptco  5874  funfvima  5950  fliftel  5999  acexmidlema  6076  acexmidlemb  6077  acexmidlem2  6082  eloprabga  6175  elrnmpo  6202  ovid  6205  offval  6310  xporderlem  6467  brtpos2  6522  issmo  6559  smores3  6564  tfrlem7  6588  tfrlem9  6590  tfr0dm  6593  tfri2  6637  rdgon  6657  freccllem  6673  frecfcllem  6675  frecsuclem  6677  el1o  6710  dif1o  6711  nnsucuniel  6768  elecg  6847  brecop  6899  erovlem  6901  oviec  6915  mapsncnv  6977  mptelixpg  7016  isfi  7047  enssdom  7048  map1  7101  xpcomco  7124  exmidpw  7215  exmidpweq  7216  tpfidceq  7237  fnfi  7250  fidcenumlemrks  7270  fidcenumlemrk  7271  djulclb  7395  eldju  7408  eldju2ndl  7412  eldju2ndr  7413  ctssdccl  7451  pw1nel3  7590  sucpw1nel3  7592  elni  7675  nlt1pig  7708  0nnq  7731  dfmq0qs  7796  dfplq0qs  7797  nqnq0  7808  elinp  7841  0npr  7850  ltdfpr  7873  nqprl  7918  nqpru  7919  addnqprlemfl  7926  addnqprlemfu  7927  mulnqprlemfl  7942  mulnqprlemfu  7943  cauappcvgprlemladdru  8023  suplocexprlemell  8080  addsrpr  8112  mulsrpr  8113  opelcn  8193  opelreal  8194  elreal  8195  elreal2  8197  0ncn  8198  addcnsr  8201  mulcnsr  8202  addvalex  8211  peano1nnnn  8219  peano2nnnn  8220  xrlenlt  8390  1nn  9316  peano2nn  9317  elnn0  9567  elnnne0  9579  un0addcl  9598  un0mulcl  9599  elxnn0  9634  uztrn2  9942  elnnuz  9961  elnn0uz  9962  elq  10024  elxr  10180  elfzm1b  10507  fz01or  10520  infssuzex  10668  infssfzcldc  10671  infssfzledc  10672  frecfzennn  10865  inftonninf  10881  seqf  10903  ser0  10972  ser0f  10973  hashinfom  11219  iswrd  11308  pfxccatpfx1  11510  clim2ser  12105  clim2ser2  12106  isermulc2  12108  iserle  12110  climserle  12113  fsum3cvg3  12165  isumclim3  12192  isumadd  12200  sumsplitdc  12201  iserabs  12244  cvgcmpub  12245  isumshft  12259  isumsplit  12260  isumlessdc  12265  cvgratz  12301  cvgratgt0  12302  clim2prod  12308  clim2divap  12309  prodf1  12311  zproddc  12348  prodsnf  12361  divides  12558  dvdsflip  12620  nninfctlemfo  12819  ialgrlemconst  12823  prm23lt5  13044  4sqlem2  13170  4sqlem12  13183  ballotfilemfrcn0  13275  ballotfilem7  13281  ennnfonelemjn  13295  ennnfonelem1  13300  ennnfonelemdm  13313  basmex  13414  ghmeqker  14076  opprringb  14388  isrhm  14467  rrgmex  14571  lssmex  14694  lidlmex  14814  2idlmex  14840  df2idl2  14848  2idlss  14853  psrbagf  15056  istps  15135  lmss  15349  txuni2  15359  dvply1  15868  sinq34lt0t  15935  logfac  16001  lgsdir2lem2  16160  gausslemma2dlem1a  16189  lgsquadlem1  16208  lgsquadlem2  16209  2sqlem1  16245  isuhgrm  16324  isushgrm  16325  isupgren  16348  isumgren  16358  umgredg  16398  umgrpredgv  16400  umgredgne  16403  umgredgnlp  16405  isuspgren  16410  isusgren  16411  ausgrusgrien  16424  usgredgppren  16450  edgssv2en  16452  uspgredg2vlem  16473  uspgredg2v  16474  ushgredgedg  16479  ushgredgedgloop  16481  griedg0ssusgr  16504  uhgrissubgr  16514  subumgredg2en  16524  uhgrspansubgrlem  16529  vtxedgfi  16542  vtxlpfi  16543  vtxdg0v  16547  wlk1walkdom  16612  clwwlkccatlem  16653  clwwlknnn  16665  clwwlknon2x  16688  bdceq  16880  bj-nntrans  16989  bj-nnelirr  16991  ss1oel2o  17029  wexmiddifxylem  17057  trilpolemisumle  17099