Theorem eleq2i 2204

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 2201	. 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 1331   e. wcel 1480

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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2119

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

This theorem is referenced by:  eleq12i  2205  eleqtri  2212  eleq2s  2232  hbxfreq  2244  abeq2i  2248  abeq1i  2249  nfceqi  2275  raleqbii  2445  rexeqbii  2446  rabeq2i  2678  elab2g  2826  elrabf  2833  elrab3t  2834  elrab2  2838  cbvsbcw  2931  cbvsbc  2932  elin2  3259  dfnul2  3360  noel  3362  rabn0m  3385  rabeq0  3387  eltpg  3564  tpid3g  3633  oprcl  3724  elunirab  3744  elintrab  3778  exss  4144  elop  4148  opm  4151  brabsb  4178  brabga  4181  pofun  4229  elsuci  4320  elsucg  4321  elsuc2g  4322  ordsucim  4411  peano2  4504  elxp  4551  brab2a  4587  brab2ga  4609  elco  4700  elcnv  4711  dmmrnm  4753  elrnmptg  4786  opelres  4819  rninxp  4977  funco  5158  elfv  5412  nfvres  5447  fvopab3g  5487  fvmptssdm  5498  fmptco  5579  funfvima  5642  fliftel  5687  acexmidlema  5758  acexmidlemb  5759  acexmidlem2  5764  eloprabga  5851  elrnmpo  5877  ovid  5880  offval  5982  xporderlem  6121  brtpos2  6141  issmo  6178  smores3  6183  tfrlem7  6207  tfrlem9  6209  tfr0dm  6212  tfri2  6256  rdgon  6276  freccllem  6292  frecfcllem  6294  frecsuclem  6296  el1o  6327  dif1o  6328  nnsucuniel  6384  elecg  6460  brecop  6512  erovlem  6514  oviec  6528  mapsncnv  6582  mptelixpg  6621  isfi  6648  enssdom  6649  map1  6699  xpcomco  6713  exmidpw  6795  fnfi  6818  fidcenumlemrks  6834  fidcenumlemrk  6835  djulclb  6933  eldju  6946  eldju2ndl  6950  eldju2ndr  6951  ctssdccl  6989  elni  7109  nlt1pig  7142  0nnq  7165  dfmq0qs  7230  dfplq0qs  7231  nqnq0  7242  elinp  7275  0npr  7284  ltdfpr  7307  nqprl  7352  nqpru  7353  addnqprlemfl  7360  addnqprlemfu  7361  mulnqprlemfl  7376  mulnqprlemfu  7377  cauappcvgprlemladdru  7457  suplocexprlemell  7514  addsrpr  7546  mulsrpr  7547  opelcn  7627  opelreal  7628  elreal  7629  elreal2  7631  0ncn  7632  addcnsr  7635  mulcnsr  7636  addvalex  7645  peano1nnnn  7653  peano2nnnn  7654  xrlenlt  7822  1nn  8724  peano2nn  8725  elnn0  8972  elnnne0  8984  un0addcl  9003  un0mulcl  9004  elxnn0  9035  uztrn2  9336  elnnuz  9355  elnn0uz  9356  elq  9407  elxr  9556  elfzm1b  9871  fz01or  9884  frecfzennn  10192  inftonninf  10207  seqf  10227  ser0  10280  ser0f  10281  hashinfom  10517  clim2ser  11099  clim2ser2  11100  isermulc2  11102  iserle  11104  climserle  11107  fsum3cvg3  11158  isumclim3  11185  isumadd  11193  sumsplitdc  11194  iserabs  11237  cvgcmpub  11238  isumshft  11252  isumsplit  11253  isumlessdc  11258  cvgratz  11294  cvgratgt0  11295  clim2prod  11301  clim2divap  11302  prodf1  11304  divides  11484  dvdsflip  11538  infssuzex  11631  ialgrlemconst  11713  ennnfonelemjn  11904  ennnfonelem1  11909  ennnfonelemdm  11922  istps  12188  lmss  12404  txuni2  12414  sinq34lt0t  12901  bdceq  13029  bj-nntrans  13138  bj-nnelirr  13140  ss1oel2o  13178  trilpolemisumle  13220