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  4369  elop  4373  opm  4376  brabsb  4405  brabga  4408  pofun  4459  elsuci  4550  elsucg  4551  elsuc2g  4552  ordsucim  4649  peano2  4744  elxp  4793  brab2a  4830  brab2ga  4852  elco  4948  elcnv  4959  dmmrnm  5003  elrnmptg  5036  opelres  5070  rninxp  5234  eliota  5368  funco  5420  elfv  5696  nfvres  5735  fvopab3g  5781  fvmptssdm  5793  fmptco  5877  funfvima  5953  fliftel  6002  acexmidlema  6079  acexmidlemb  6080  acexmidlem2  6085  eloprabga  6178  elrnmpo  6205  ovid  6208  offval  6314  xporderlem  6471  brtpos2  6527  issmo  6564  smores3  6569  tfrlem7  6593  tfrlem9  6595  tfr0dm  6598  tfri2  6642  rdgon  6662  freccllem  6678  frecfcllem  6680  frecsuclem  6682  el1o  6715  dif1o  6716  nnsucuniel  6773  elecg  6852  brecop  6904  erovlem  6906  oviec  6920  mapsncnv  6983  mptelixpg  7022  isfi  7053  enssdom  7054  map1  7107  xpcomco  7130  exmidpw  7221  exmidpweq  7222  tpfidceq  7243  fnfi  7256  fidcenumlemrks  7277  fidcenumlemrk  7278  djulclb  7402  eldju  7415  eldju2ndl  7419  eldju2ndr  7420  ctssdccl  7458  pw1nel3  7597  sucpw1nel3  7599  elni  7682  nlt1pig  7715  0nnq  7738  dfmq0qs  7803  dfplq0qs  7804  nqnq0  7815  elinp  7848  0npr  7857  ltdfpr  7880  nqprl  7925  nqpru  7926  addnqprlemfl  7933  addnqprlemfu  7934  mulnqprlemfl  7949  mulnqprlemfu  7950  cauappcvgprlemladdru  8030  suplocexprlemell  8087  addsrpr  8119  mulsrpr  8120  opelcn  8200  opelreal  8201  elreal  8202  elreal2  8204  0ncn  8205  addcnsr  8208  mulcnsr  8209  addvalex  8218  peano1nnnn  8226  peano2nnnn  8227  xrlenlt  8397  1nn  9325  peano2nn  9326  elnn0  9577  elnnne0  9589  un0addcl  9608  un0mulcl  9609  elxnn0  9642  uztrn2  9956  elnnuz  9975  elnn0uz  9976  elq  10038  elxr  10195  elfzm1b  10522  fz01or  10535  infssuzex  10683  infssfzcldc  10686  infssfzledc  10687  frecfzennn  10884  inftonninf  10900  seqf  10922  ser0  10991  ser0f  10992  hashinfom  11239  iswrd  11328  pfxccatpfx1  11530  clim2ser  12128  clim2ser2  12129  isermulc2  12131  iserle  12133  climserle  12136  fsum3cvg3  12188  isumclim3  12215  isumadd  12223  sumsplitdc  12224  iserabs  12267  cvgcmpub  12268  isumshft  12282  isumsplit  12283  isumlessdc  12288  cvgratz  12324  cvgratgt0  12325  clim2prod  12331  clim2divap  12332  prodf1  12334  zproddc  12371  prodsnf  12384  divides  12581  dvdsflip  12643  nninfctlemfo  12842  ialgrlemconst  12846  prm23lt5  13071  4sqlem2  13197  4sqlem12  13210  ballotfilemfrcn0  13331  ballotfilem7  13337  ennnfonelemjn  13351  ennnfonelem1  13356  ennnfonelemdm  13369  basmex  13470  ghmeqker  14133  elcntr  14163  cntri  14165  cntzsgrpcl  14167  idjusnfi  14270  opprringb  14495  isrhm  14574  rrgmex  14678  lssmex  14801  lidlmex  14921  2idlmex  14947  df2idl2  14955  2idlss  14960  psrbagf  15165  psrbagconclfi  15182  istps  15291  lmss  15505  txuni2  15515  dvply1  16024  sinq34lt0t  16091  logfac  16159  ppiublem1  16324  lgsdir2lem2  16386  gausslemma2dlem1a  16415  lgsquadlem1  16434  lgsquadlem2  16435  2sqlem1  16471  isuhgrm  16550  isushgrm  16551  isupgren  16574  isumgren  16584  umgredg  16624  umgrpredgv  16626  umgredgne  16629  umgredgnlp  16631  isuspgren  16636  isusgren  16637  ausgrusgrien  16650  usgredgppren  16676  edgssv2en  16678  uspgredg2vlem  16699  uspgredg2v  16700  ushgredgedg  16705  ushgredgedgloop  16707  griedg0ssusgr  16730  uhgrissubgr  16740  subumgredg2en  16750  uhgrspansubgrlem  16755  vtxedgfi  16768  vtxlpfi  16769  vtxdg0v  16773  wlk1walkdom  16838  clwwlkccatlem  16879  clwwlknnn  16891  clwwlknon2x  16914  bdceq  17106  bj-nntrans  17215  bj-nnelirr  17217  ss1oel2o  17255  wexmiddifxylem  17283  idjudju  17285  trilpolemisumle  17327