Theorem eleq2i 2232

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 2229	. 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 1343   e. wcel 2136

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 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158  df-clel 2161

This theorem is referenced by:  eleq12i  2233  eleqtri  2240  eleq2s  2260  hbxfreq  2272  abeq2i  2276  abeq1i  2277  nfceqi  2303  raleqbii  2477  rexeqbii  2478  rabeq2i  2722  elab2g  2872  elrabf  2879  elrab3t  2880  elrab2  2884  cbvsbcw  2977  cbvsbc  2978  csbcow  3055  elin2  3309  dfnul2  3410  noel  3412  rabn0m  3435  rabeq0  3437  eltpg  3620  tpid3g  3690  oprcl  3781  elunirab  3801  elintrab  3835  exss  4204  elop  4208  opm  4211  brabsb  4238  brabga  4241  pofun  4289  elsuci  4380  elsucg  4381  elsuc2g  4382  ordsucim  4476  peano2  4571  elxp  4620  brab2a  4656  brab2ga  4678  elco  4769  elcnv  4780  dmmrnm  4822  elrnmptg  4855  opelres  4888  rninxp  5046  funco  5227  elfv  5483  nfvres  5518  fvopab3g  5558  fvmptssdm  5569  fmptco  5650  funfvima  5715  fliftel  5760  acexmidlema  5832  acexmidlemb  5833  acexmidlem2  5838  eloprabga  5925  elrnmpo  5951  ovid  5954  offval  6056  xporderlem  6195  brtpos2  6215  issmo  6252  smores3  6257  tfrlem7  6281  tfrlem9  6283  tfr0dm  6286  tfri2  6330  rdgon  6350  freccllem  6366  frecfcllem  6368  frecsuclem  6370  el1o  6401  dif1o  6402  nnsucuniel  6459  elecg  6535  brecop  6587  erovlem  6589  oviec  6603  mapsncnv  6657  mptelixpg  6696  isfi  6723  enssdom  6724  map1  6774  xpcomco  6788  exmidpw  6870  exmidpweq  6871  fnfi  6898  fidcenumlemrks  6914  fidcenumlemrk  6915  djulclb  7016  eldju  7029  eldju2ndl  7033  eldju2ndr  7034  ctssdccl  7072  pw1nel3  7183  sucpw1nel3  7185  elni  7245  nlt1pig  7278  0nnq  7301  dfmq0qs  7366  dfplq0qs  7367  nqnq0  7378  elinp  7411  0npr  7420  ltdfpr  7443  nqprl  7488  nqpru  7489  addnqprlemfl  7496  addnqprlemfu  7497  mulnqprlemfl  7512  mulnqprlemfu  7513  cauappcvgprlemladdru  7593  suplocexprlemell  7650  addsrpr  7682  mulsrpr  7683  opelcn  7763  opelreal  7764  elreal  7765  elreal2  7767  0ncn  7768  addcnsr  7771  mulcnsr  7772  addvalex  7781  peano1nnnn  7789  peano2nnnn  7790  xrlenlt  7959  1nn  8864  peano2nn  8865  elnn0  9112  elnnne0  9124  un0addcl  9143  un0mulcl  9144  elxnn0  9175  uztrn2  9479  elnnuz  9498  elnn0uz  9499  elq  9556  elxr  9708  elfzm1b  10029  fz01or  10042  frecfzennn  10357  inftonninf  10372  seqf  10392  ser0  10445  ser0f  10446  hashinfom  10687  clim2ser  11274  clim2ser2  11275  isermulc2  11277  iserle  11279  climserle  11282  fsum3cvg3  11333  isumclim3  11360  isumadd  11368  sumsplitdc  11369  iserabs  11412  cvgcmpub  11413  isumshft  11427  isumsplit  11428  isumlessdc  11433  cvgratz  11469  cvgratgt0  11470  clim2prod  11476  clim2divap  11477  prodf1  11479  zproddc  11516  prodsnf  11529  divides  11725  dvdsflip  11785  infssuzex  11878  ialgrlemconst  11971  prm23lt5  12191  4sqlem2  12315  ennnfonelemjn  12331  ennnfonelem1  12336  ennnfonelemdm  12349  istps  12630  lmss  12846  txuni2  12856  sinq34lt0t  13352  lgsdir2lem2  13530  2sqlem1  13550  bdceq  13684  bj-nntrans  13793  bj-nnelirr  13795  ss1oel2o  13833  trilpolemisumle  13877