Theorem eleq2i 2206

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 2203	. 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 2121

This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135

This theorem is referenced by:  eleq12i  2207  eleqtri  2214  eleq2s  2234  hbxfreq  2246  abeq2i  2250  abeq1i  2251  nfceqi  2277  raleqbii  2447  rexeqbii  2448  rabeq2i  2683  elab2g  2831  elrabf  2838  elrab3t  2839  elrab2  2843  cbvsbcw  2936  cbvsbc  2937  elin2  3264  dfnul2  3365  noel  3367  rabn0m  3390  rabeq0  3392  eltpg  3569  tpid3g  3638  oprcl  3729  elunirab  3749  elintrab  3783  exss  4149  elop  4153  opm  4156  brabsb  4183  brabga  4186  pofun  4234  elsuci  4325  elsucg  4326  elsuc2g  4327  ordsucim  4416  peano2  4509  elxp  4556  brab2a  4592  brab2ga  4614  elco  4705  elcnv  4716  dmmrnm  4758  elrnmptg  4791  opelres  4824  rninxp  4982  funco  5163  elfv  5419  nfvres  5454  fvopab3g  5494  fvmptssdm  5505  fmptco  5586  funfvima  5649  fliftel  5694  acexmidlema  5765  acexmidlemb  5766  acexmidlem2  5771  eloprabga  5858  elrnmpo  5884  ovid  5887  offval  5989  xporderlem  6128  brtpos2  6148  issmo  6185  smores3  6190  tfrlem7  6214  tfrlem9  6216  tfr0dm  6219  tfri2  6263  rdgon  6283  freccllem  6299  frecfcllem  6301  frecsuclem  6303  el1o  6334  dif1o  6335  nnsucuniel  6391  elecg  6467  brecop  6519  erovlem  6521  oviec  6535  mapsncnv  6589  mptelixpg  6628  isfi  6655  enssdom  6656  map1  6706  xpcomco  6720  exmidpw  6802  fnfi  6825  fidcenumlemrks  6841  fidcenumlemrk  6842  djulclb  6940  eldju  6953  eldju2ndl  6957  eldju2ndr  6958  ctssdccl  6996  elni  7121  nlt1pig  7154  0nnq  7177  dfmq0qs  7242  dfplq0qs  7243  nqnq0  7254  elinp  7287  0npr  7296  ltdfpr  7319  nqprl  7364  nqpru  7365  addnqprlemfl  7372  addnqprlemfu  7373  mulnqprlemfl  7388  mulnqprlemfu  7389  cauappcvgprlemladdru  7469  suplocexprlemell  7526  addsrpr  7558  mulsrpr  7559  opelcn  7639  opelreal  7640  elreal  7641  elreal2  7643  0ncn  7644  addcnsr  7647  mulcnsr  7648  addvalex  7657  peano1nnnn  7665  peano2nnnn  7666  xrlenlt  7834  1nn  8736  peano2nn  8737  elnn0  8984  elnnne0  8996  un0addcl  9015  un0mulcl  9016  elxnn0  9047  uztrn2  9348  elnnuz  9367  elnn0uz  9368  elq  9419  elxr  9568  elfzm1b  9883  fz01or  9896  frecfzennn  10204  inftonninf  10219  seqf  10239  ser0  10292  ser0f  10293  hashinfom  10529  clim2ser  11111  clim2ser2  11112  isermulc2  11114  iserle  11116  climserle  11119  fsum3cvg3  11170  isumclim3  11197  isumadd  11205  sumsplitdc  11206  iserabs  11249  cvgcmpub  11250  isumshft  11264  isumsplit  11265  isumlessdc  11270  cvgratz  11306  cvgratgt0  11307  clim2prod  11313  clim2divap  11314  prodf1  11316  divides  11500  dvdsflip  11554  infssuzex  11647  ialgrlemconst  11729  ennnfonelemjn  11920  ennnfonelem1  11925  ennnfonelemdm  11938  istps  12204  lmss  12420  txuni2  12430  sinq34lt0t  12917  bdceq  13045  bj-nntrans  13154  bj-nnelirr  13156  ss1oel2o  13194  trilpolemisumle  13236