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  2797  elab2g  2951  elrabf  2958  elrab3t  2959  elrab2  2963  cbvsbcw  3057  cbvsbc  3058  csbcow  3136  elin2  3393  dfnul2  3494  noel  3496  rabn0m  3520  rabeq0  3522  eltpg  3712  tpid3g  3785  oprcl  3884  elunirab  3904  elintrab  3938  exss  4317  elop  4321  opm  4324  brabsb  4353  brabga  4356  pofun  4407  elsuci  4498  elsucg  4499  elsuc2g  4500  ordsucim  4596  peano2  4691  elxp  4740  brab2a  4777  brab2ga  4799  elco  4894  elcnv  4905  dmmrnm  4949  elrnmptg  4982  opelres  5016  rninxp  5178  eliota  5312  funco  5364  elfv  5633  nfvres  5671  fvopab3g  5715  fvmptssdm  5727  fmptco  5809  funfvima  5881  fliftel  5929  acexmidlema  6004  acexmidlemb  6005  acexmidlem2  6010  eloprabga  6103  elrnmpo  6130  ovid  6133  offval  6238  xporderlem  6391  brtpos2  6412  issmo  6449  smores3  6454  tfrlem7  6478  tfrlem9  6480  tfr0dm  6483  tfri2  6527  rdgon  6547  freccllem  6563  frecfcllem  6565  frecsuclem  6567  el1o  6600  dif1o  6601  nnsucuniel  6658  elecg  6737  brecop  6789  erovlem  6791  oviec  6805  mapsncnv  6859  mptelixpg  6898  isfi  6929  enssdom  6930  map1  6982  xpcomco  7005  exmidpw  7095  exmidpweq  7096  tpfidceq  7117  fnfi  7129  fidcenumlemrks  7146  fidcenumlemrk  7147  djulclb  7248  eldju  7261  eldju2ndl  7265  eldju2ndr  7266  ctssdccl  7304  pw1nel3  7442  sucpw1nel3  7444  elni  7521  nlt1pig  7554  0nnq  7577  dfmq0qs  7642  dfplq0qs  7643  nqnq0  7654  elinp  7687  0npr  7696  ltdfpr  7719  nqprl  7764  nqpru  7765  addnqprlemfl  7772  addnqprlemfu  7773  mulnqprlemfl  7788  mulnqprlemfu  7789  cauappcvgprlemladdru  7869  suplocexprlemell  7926  addsrpr  7958  mulsrpr  7959  opelcn  8039  opelreal  8040  elreal  8041  elreal2  8043  0ncn  8044  addcnsr  8047  mulcnsr  8048  addvalex  8057  peano1nnnn  8065  peano2nnnn  8066  xrlenlt  8237  1nn  9147  peano2nn  9148  elnn0  9397  elnnne0  9409  un0addcl  9428  un0mulcl  9429  elxnn0  9460  uztrn2  9767  elnnuz  9786  elnn0uz  9787  elq  9849  elxr  10004  elfzm1b  10326  fz01or  10339  infssuzex  10486  frecfzennn  10681  inftonninf  10697  seqf  10719  ser0  10788  ser0f  10789  hashinfom  11033  iswrd  11108  pfxccatpfx1  11310  clim2ser  11891  clim2ser2  11892  isermulc2  11894  iserle  11896  climserle  11899  fsum3cvg3  11950  isumclim3  11977  isumadd  11985  sumsplitdc  11986  iserabs  12029  cvgcmpub  12030  isumshft  12044  isumsplit  12045  isumlessdc  12050  cvgratz  12086  cvgratgt0  12087  clim2prod  12093  clim2divap  12094  prodf1  12096  zproddc  12133  prodsnf  12146  divides  12343  dvdsflip  12405  nninfctlemfo  12604  ialgrlemconst  12608  prm23lt5  12829  4sqlem2  12955  4sqlem12  12968  ennnfonelemjn  13016  ennnfonelem1  13021  ennnfonelemdm  13034  basmex  13135  ghmeqker  13851  isrhm  14165  rrgmex  14268  lssmex  14362  lidlmex  14482  2idlmex  14508  df2idl2  14516  2idlss  14521  psrbagf  14677  istps  14749  lmss  14963  txuni2  14973  dvply1  15482  sinq34lt0t  15548  lgsdir2lem2  15751  gausslemma2dlem1a  15780  lgsquadlem1  15799  lgsquadlem2  15800  2sqlem1  15836  isuhgrm  15915  isushgrm  15916  isupgren  15939  isumgren  15949  umgredg  15989  umgrpredgv  15991  umgredgne  15994  umgredgnlp  15996  isuspgren  16001  isusgren  16002  ausgrusgrien  16015  usgredgppren  16041  edgssv2en  16043  uspgredg2vlem  16064  uspgredg2v  16065  ushgredgedg  16070  ushgredgedgloop  16072  griedg0ssusgr  16095  vtxedgfi  16100  vtxlpfi  16101  vtxdg0v  16105  wlk1walkdom  16170  clwwlkccatlem  16209  clwwlknnn  16221  clwwlknon2x  16244  bdceq  16387  bj-nntrans  16496  bj-nnelirr  16498  ss1oel2o  16536  trilpolemisumle  16592