Theorem eleq2i 2301

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 2298	. 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 1398   e. wcel 2205

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-clel 2230

This theorem is referenced by:  eleq12i  2302  eleqtri  2309  eleq2s  2329  hbxfreq  2341  abeq2i  2345  abeq1i  2346  nfceqi  2382  raleqbii  2556  rexeqbii  2557  reqabi  2722  rabeq2i  2812  elab2g  2966  elrabf  2973  elrab3t  2974  elrab2  2978  cbvsbcw  3072  cbvsbc  3073  csbcow  3151  elin2  3409  dfnul2  3512  noel  3514  rabn0m  3538  rabeq0  3540  eltpg  3736  tpid3g  3809  oprcl  3909  elunirab  3929  elintrab  3963  exss  4345  elop  4349  opm  4352  brabsb  4381  brabga  4384  pofun  4435  elsuci  4526  elsucg  4527  elsuc2g  4528  ordsucim  4624  peano2  4719  elxp  4768  brab2a  4805  brab2ga  4827  elco  4923  elcnv  4934  dmmrnm  4978  elrnmptg  5011  opelres  5045  rninxp  5208  eliota  5342  funco  5394  elfv  5670  nfvres  5708  fvopab3g  5752  fvmptssdm  5764  fmptco  5845  funfvima  5920  fliftel  5968  acexmidlema  6043  acexmidlemb  6044  acexmidlem2  6049  eloprabga  6142  elrnmpo  6169  ovid  6172  offval  6276  xporderlem  6429  brtpos2  6484  issmo  6521  smores3  6526  tfrlem7  6550  tfrlem9  6552  tfr0dm  6555  tfri2  6599  rdgon  6619  freccllem  6635  frecfcllem  6637  frecsuclem  6639  el1o  6672  dif1o  6673  nnsucuniel  6730  elecg  6809  brecop  6861  erovlem  6863  oviec  6877  mapsncnv  6932  mptelixpg  6971  isfi  7002  enssdom  7003  map1  7056  xpcomco  7079  exmidpw  7170  exmidpweq  7171  tpfidceq  7192  fnfi  7205  fidcenumlemrks  7225  fidcenumlemrk  7226  djulclb  7348  eldju  7361  eldju2ndl  7365  eldju2ndr  7366  ctssdccl  7404  pw1nel3  7543  sucpw1nel3  7545  elni  7625  nlt1pig  7658  0nnq  7681  dfmq0qs  7746  dfplq0qs  7747  nqnq0  7758  elinp  7791  0npr  7800  ltdfpr  7823  nqprl  7868  nqpru  7869  addnqprlemfl  7876  addnqprlemfu  7877  mulnqprlemfl  7892  mulnqprlemfu  7893  cauappcvgprlemladdru  7973  suplocexprlemell  8030  addsrpr  8062  mulsrpr  8063  opelcn  8143  opelreal  8144  elreal  8145  elreal2  8147  0ncn  8148  addcnsr  8151  mulcnsr  8152  addvalex  8161  peano1nnnn  8169  peano2nnnn  8170  xrlenlt  8340  1nn  9250  peano2nn  9251  elnn0  9500  elnnne0  9512  un0addcl  9531  un0mulcl  9532  elxnn0  9567  uztrn2  9875  elnnuz  9894  elnn0uz  9895  elq  9957  elxr  10112  elfzm1b  10436  fz01or  10449  infssuzex  10597  frecfzennn  10792  inftonninf  10808  seqf  10830  ser0  10899  ser0f  10900  hashinfom  11145  iswrd  11230  pfxccatpfx1  11432  clim2ser  12026  clim2ser2  12027  isermulc2  12029  iserle  12031  climserle  12034  fsum3cvg3  12086  isumclim3  12113  isumadd  12121  sumsplitdc  12122  iserabs  12165  cvgcmpub  12166  isumshft  12180  isumsplit  12181  isumlessdc  12186  cvgratz  12222  cvgratgt0  12223  clim2prod  12229  clim2divap  12230  prodf1  12232  zproddc  12269  prodsnf  12282  divides  12479  dvdsflip  12541  nninfctlemfo  12740  ialgrlemconst  12744  prm23lt5  12965  4sqlem2  13091  4sqlem12  13104  ennnfonelemjn  13170  ennnfonelem1  13175  ennnfonelemdm  13188  basmex  13289  ghmeqker  14005  isrhm  14320  rrgmex  14423  lssmex  14520  lidlmex  14640  2idlmex  14666  df2idl2  14674  2idlss  14679  psrbagf  14835  istps  14914  lmss  15128  txuni2  15138  dvply1  15647  sinq34lt0t  15713  lgsdir2lem2  15919  gausslemma2dlem1a  15948  lgsquadlem1  15967  lgsquadlem2  15968  2sqlem1  16004  isuhgrm  16083  isushgrm  16084  isupgren  16107  isumgren  16117  umgredg  16157  umgrpredgv  16159  umgredgne  16162  umgredgnlp  16164  isuspgren  16169  isusgren  16170  ausgrusgrien  16183  usgredgppren  16209  edgssv2en  16211  uspgredg2vlem  16232  uspgredg2v  16233  ushgredgedg  16238  ushgredgedgloop  16240  griedg0ssusgr  16263  uhgrissubgr  16273  subumgredg2en  16283  uhgrspansubgrlem  16288  vtxedgfi  16301  vtxlpfi  16302  vtxdg0v  16306  wlk1walkdom  16371  clwwlkccatlem  16412  clwwlknnn  16424  clwwlknon2x  16447  bdceq  16629  bj-nntrans  16738  bj-nnelirr  16740  ss1oel2o  16778  trilpolemisumle  16839