Theorem eleq2i 2244

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 2241	. 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 1353   e. wcel 2148

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173

This theorem is referenced by:  eleq12i  2245  eleqtri  2252  eleq2s  2272  hbxfreq  2284  abeq2i  2288  abeq1i  2289  nfceqi  2315  raleqbii  2489  rexeqbii  2490  rabeq2i  2736  elab2g  2886  elrabf  2893  elrab3t  2894  elrab2  2898  cbvsbcw  2992  cbvsbc  2993  csbcow  3070  elin2  3325  dfnul2  3426  noel  3428  rabn0m  3452  rabeq0  3454  eltpg  3639  tpid3g  3709  oprcl  3804  elunirab  3824  elintrab  3858  exss  4229  elop  4233  opm  4236  brabsb  4263  brabga  4266  pofun  4314  elsuci  4405  elsucg  4406  elsuc2g  4407  ordsucim  4501  peano2  4596  elxp  4645  brab2a  4681  brab2ga  4703  elco  4795  elcnv  4806  dmmrnm  4848  elrnmptg  4881  opelres  4914  rninxp  5074  eliota  5206  funco  5258  elfv  5515  nfvres  5550  fvopab3g  5592  fvmptssdm  5603  fmptco  5685  funfvima  5751  fliftel  5797  acexmidlema  5869  acexmidlemb  5870  acexmidlem2  5875  eloprabga  5965  elrnmpo  5991  ovid  5994  offval  6093  xporderlem  6235  brtpos2  6255  issmo  6292  smores3  6297  tfrlem7  6321  tfrlem9  6323  tfr0dm  6326  tfri2  6370  rdgon  6390  freccllem  6406  frecfcllem  6408  frecsuclem  6410  el1o  6441  dif1o  6442  nnsucuniel  6499  elecg  6576  brecop  6628  erovlem  6630  oviec  6644  mapsncnv  6698  mptelixpg  6737  isfi  6764  enssdom  6765  map1  6815  xpcomco  6829  exmidpw  6911  exmidpweq  6912  fnfi  6939  fidcenumlemrks  6955  fidcenumlemrk  6956  djulclb  7057  eldju  7070  eldju2ndl  7074  eldju2ndr  7075  ctssdccl  7113  pw1nel3  7233  sucpw1nel3  7235  elni  7310  nlt1pig  7343  0nnq  7366  dfmq0qs  7431  dfplq0qs  7432  nqnq0  7443  elinp  7476  0npr  7485  ltdfpr  7508  nqprl  7553  nqpru  7554  addnqprlemfl  7561  addnqprlemfu  7562  mulnqprlemfl  7577  mulnqprlemfu  7578  cauappcvgprlemladdru  7658  suplocexprlemell  7715  addsrpr  7747  mulsrpr  7748  opelcn  7828  opelreal  7829  elreal  7830  elreal2  7832  0ncn  7833  addcnsr  7836  mulcnsr  7837  addvalex  7846  peano1nnnn  7854  peano2nnnn  7855  xrlenlt  8025  1nn  8933  peano2nn  8934  elnn0  9181  elnnne0  9193  un0addcl  9212  un0mulcl  9213  elxnn0  9244  uztrn2  9548  elnnuz  9567  elnn0uz  9568  elq  9625  elxr  9779  elfzm1b  10101  fz01or  10114  frecfzennn  10429  inftonninf  10444  seqf  10464  ser0  10517  ser0f  10518  hashinfom  10761  clim2ser  11348  clim2ser2  11349  isermulc2  11351  iserle  11353  climserle  11356  fsum3cvg3  11407  isumclim3  11434  isumadd  11442  sumsplitdc  11443  iserabs  11486  cvgcmpub  11487  isumshft  11501  isumsplit  11502  isumlessdc  11507  cvgratz  11543  cvgratgt0  11544  clim2prod  11550  clim2divap  11551  prodf1  11553  zproddc  11590  prodsnf  11603  divides  11799  dvdsflip  11860  infssuzex  11953  ialgrlemconst  12046  prm23lt5  12266  4sqlem2  12390  ennnfonelemjn  12406  ennnfonelem1  12411  ennnfonelemdm  12424  basmex  12524  lidlmex  13564  istps  13672  lmss  13886  txuni2  13896  sinq34lt0t  14392  lgsdir2lem2  14570  2sqlem1  14601  bdceq  14734  bj-nntrans  14843  bj-nnelirr  14845  ss1oel2o  14883  trilpolemisumle  14926