Theorem eleq2i 2207

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 2204	. 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 104   = wceq 1332   e. wcel 1481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-cleq 2133  df-clel 2136

This theorem is referenced by:  eleq12i  2208  eleqtri  2215  eleq2s  2235  hbxfreq  2247  abeq2i  2251  abeq1i  2252  nfceqi  2278  raleqbii  2450  rexeqbii  2451  rabeq2i  2686  elab2g  2835  elrabf  2842  elrab3t  2843  elrab2  2847  cbvsbcw  2940  cbvsbc  2941  elin2  3269  dfnul2  3370  noel  3372  rabn0m  3395  rabeq0  3397  eltpg  3576  tpid3g  3646  oprcl  3737  elunirab  3757  elintrab  3791  exss  4157  elop  4161  opm  4164  brabsb  4191  brabga  4194  pofun  4242  elsuci  4333  elsucg  4334  elsuc2g  4335  ordsucim  4424  peano2  4517  elxp  4564  brab2a  4600  brab2ga  4622  elco  4713  elcnv  4724  dmmrnm  4766  elrnmptg  4799  opelres  4832  rninxp  4990  funco  5171  elfv  5427  nfvres  5462  fvopab3g  5502  fvmptssdm  5513  fmptco  5594  funfvima  5657  fliftel  5702  acexmidlema  5773  acexmidlemb  5774  acexmidlem2  5779  eloprabga  5866  elrnmpo  5892  ovid  5895  offval  5997  xporderlem  6136  brtpos2  6156  issmo  6193  smores3  6198  tfrlem7  6222  tfrlem9  6224  tfr0dm  6227  tfri2  6271  rdgon  6291  freccllem  6307  frecfcllem  6309  frecsuclem  6311  el1o  6342  dif1o  6343  nnsucuniel  6399  elecg  6475  brecop  6527  erovlem  6529  oviec  6543  mapsncnv  6597  mptelixpg  6636  isfi  6663  enssdom  6664  map1  6714  xpcomco  6728  exmidpw  6810  fnfi  6833  fidcenumlemrks  6849  fidcenumlemrk  6850  djulclb  6948  eldju  6961  eldju2ndl  6965  eldju2ndr  6966  ctssdccl  7004  elni  7140  nlt1pig  7173  0nnq  7196  dfmq0qs  7261  dfplq0qs  7262  nqnq0  7273  elinp  7306  0npr  7315  ltdfpr  7338  nqprl  7383  nqpru  7384  addnqprlemfl  7391  addnqprlemfu  7392  mulnqprlemfl  7407  mulnqprlemfu  7408  cauappcvgprlemladdru  7488  suplocexprlemell  7545  addsrpr  7577  mulsrpr  7578  opelcn  7658  opelreal  7659  elreal  7660  elreal2  7662  0ncn  7663  addcnsr  7666  mulcnsr  7667  addvalex  7676  peano1nnnn  7684  peano2nnnn  7685  xrlenlt  7853  1nn  8755  peano2nn  8756  elnn0  9003  elnnne0  9015  un0addcl  9034  un0mulcl  9035  elxnn0  9066  uztrn2  9367  elnnuz  9386  elnn0uz  9387  elq  9441  elxr  9593  elfzm1b  9909  fz01or  9922  frecfzennn  10230  inftonninf  10245  seqf  10265  ser0  10318  ser0f  10319  hashinfom  10556  clim2ser  11138  clim2ser2  11139  isermulc2  11141  iserle  11143  climserle  11146  fsum3cvg3  11197  isumclim3  11224  isumadd  11232  sumsplitdc  11233  iserabs  11276  cvgcmpub  11277  isumshft  11291  isumsplit  11292  isumlessdc  11297  cvgratz  11333  cvgratgt0  11334  clim2prod  11340  clim2divap  11341  prodf1  11343  zproddc  11380  divides  11531  dvdsflip  11585  infssuzex  11678  ialgrlemconst  11760  ennnfonelemjn  11951  ennnfonelem1  11956  ennnfonelemdm  11969  istps  12238  lmss  12454  txuni2  12464  sinq34lt0t  12960  bdceq  13211  bj-nntrans  13320  bj-nnelirr  13322  ss1oel2o  13360  trilpolemisumle  13406