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  7396  eldju  7409  eldju2ndl  7413  eldju2ndr  7414  ctssdccl  7452  pw1nel3  7591  sucpw1nel3  7593  elni  7676  nlt1pig  7709  0nnq  7732  dfmq0qs  7797  dfplq0qs  7798  nqnq0  7809  elinp  7842  0npr  7851  ltdfpr  7874  nqprl  7919  nqpru  7920  addnqprlemfl  7927  addnqprlemfu  7928  mulnqprlemfl  7943  mulnqprlemfu  7944  cauappcvgprlemladdru  8024  suplocexprlemell  8081  addsrpr  8113  mulsrpr  8114  opelcn  8194  opelreal  8195  elreal  8196  elreal2  8198  0ncn  8199  addcnsr  8202  mulcnsr  8203  addvalex  8212  peano1nnnn  8220  peano2nnnn  8221  xrlenlt  8391  1nn  9318  peano2nn  9319  elnn0  9570  elnnne0  9582  un0addcl  9601  un0mulcl  9602  elxnn0  9637  uztrn2  9950  elnnuz  9969  elnn0uz  9970  elq  10032  elxr  10189  elfzm1b  10516  fz01or  10529  infssuzex  10677  infssfzcldc  10680  infssfzledc  10681  frecfzennn  10877  inftonninf  10893  seqf  10915  ser0  10984  ser0f  10985  hashinfom  11232  iswrd  11321  pfxccatpfx1  11523  clim2ser  12121  clim2ser2  12122  isermulc2  12124  iserle  12126  climserle  12129  fsum3cvg3  12181  isumclim3  12208  isumadd  12216  sumsplitdc  12217  iserabs  12260  cvgcmpub  12261  isumshft  12275  isumsplit  12276  isumlessdc  12281  cvgratz  12317  cvgratgt0  12318  clim2prod  12324  clim2divap  12325  prodf1  12327  zproddc  12364  prodsnf  12377  divides  12574  dvdsflip  12636  nninfctlemfo  12835  ialgrlemconst  12839  prm23lt5  13064  4sqlem2  13190  4sqlem12  13203  ballotfilemfrcn0  13324  ballotfilem7  13330  ennnfonelemjn  13344  ennnfonelem1  13349  ennnfonelemdm  13362  basmex  13463  ghmeqker  14125  opprringb  14437  isrhm  14516  rrgmex  14620  lssmex  14743  lidlmex  14863  2idlmex  14889  df2idl2  14897  2idlss  14902  psrbagf  15105  istps  15185  lmss  15399  txuni2  15409  dvply1  15918  sinq34lt0t  15985  logfac  16051  ppiublem1  16213  lgsdir2lem2  16270  gausslemma2dlem1a  16299  lgsquadlem1  16318  lgsquadlem2  16319  2sqlem1  16355  isuhgrm  16434  isushgrm  16435  isupgren  16458  isumgren  16468  umgredg  16508  umgrpredgv  16510  umgredgne  16513  umgredgnlp  16515  isuspgren  16520  isusgren  16521  ausgrusgrien  16534  usgredgppren  16560  edgssv2en  16562  uspgredg2vlem  16583  uspgredg2v  16584  ushgredgedg  16589  ushgredgedgloop  16591  griedg0ssusgr  16614  uhgrissubgr  16624  subumgredg2en  16634  uhgrspansubgrlem  16639  vtxedgfi  16652  vtxlpfi  16653  vtxdg0v  16657  wlk1walkdom  16722  clwwlkccatlem  16763  clwwlknnn  16775  clwwlknon2x  16798  bdceq  16990  bj-nntrans  17099  bj-nnelirr  17101  ss1oel2o  17139  wexmiddifxylem  17167  trilpolemisumle  17209